SUCCESS: Derivation has unique formula names SUCCESS: All derived formulae have parents and inference information SUCCESS: Derivation is acyclic SUCCESS: Assumptions are propagated SUCCESS: Assumptions are discharged RESULT: axioms.sat_model.dis - Paradox---4.0 says Satisfiable - CPU = 0.00 SUCCESS: Leaf axioms are satisfiable RESULT: i1.thm.dis - Otter---3.3 says Theorem - CPU = 1.80 SUCCESS: i1 is a thm of a4 a10 RESULT: addi1.thm.dis - Otter---3.3 says Theorem - CPU = 1.85 SUCCESS: addi1 is a thm of a3 i1 RESULT: i2.thm.dis - Otter---3.3 says GaveUp - CPU = 1.87 RESULT: i2.thm.dis - Paradox---4.0 says CounterSatisfiable - CPU = 0.00 FAILURE: i2 is not a thm of a3 i1 RESULT: i3.thm.dis - Otter---3.3 says Theorem - CPU = 1.82 SUCCESS: i3 is a thm of a2_1 i2 RESULT: i4.thm.dis - Otter---3.3 says Theorem - CPU = 1.85 SUCCESS: i4 is a thm of a10 a5 a6 a4 RESULT: i5.thm.dis - Otter---3.3 says GaveUp - CPU = 1.88 RESULT: i5.thm.dis - Paradox---4.0 says CounterSatisfiable - CPU = 0.00 FAILURE: i5 is not a thm of a7 i4 RESULT: i6.thm.dis - Otter---3.3 says Theorem - CPU = 1.92 SUCCESS: i6 is a thm of i5 a2_1 RESULT: i7.thm.dis - Otter---3.3 says Theorem - CPU = 1.86 SUCCESS: i7 is a thm of i3 i6 a9 a10 a0 a1_1 a1_2 CPUTIME: 18.44 FAILURE: Not verifiedSZS status NotVerified