%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SEV610+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 06:51:59 PM UTC 2026 % Result : Theorem 0.39s 0.65s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEV610+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.15/0.33 % Computer : n011.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue May 5 05:30:32 EDT 2026 % 0.15/0.34 % CPUTime : % 0.29/0.54 # SinE strategy is gf120_h_gu_RUU_F100_L00500 % 0.29/0.54 # Auto-Mode selected heuristic G_E___207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2SI % 0.29/0.54 # and selection function SelectNewComplexAHP. % 0.29/0.54 # % 0.29/0.54 # Presaturation interreduction done % 0.29/0.54 # Number of axioms: 104 Number of unprocessed: 94 % 0.29/0.54 # Tableaux proof search. % 0.29/0.54 # APR header successfully linked. % 0.29/0.54 # Hello from C++ % 0.29/0.54 # The folding up rule is enabled... % 0.29/0.54 # Local unification is enabled... % 0.29/0.54 # Any saturation attempts will use folding labels... % 0.29/0.54 # 94 beginning clauses after preprocessing and clausification % 0.29/0.54 # Creating start rules for all 3 conjectures. % 0.29/0.54 # There are 3 start rule candidates: % 0.29/0.54 # Found 4 unit axioms. % 0.29/0.54 # Unsuccessfully attempted saturation on 1 start tableaux, moving on. % 0.29/0.54 # 3 start rule tableaux created. % 0.29/0.54 # 90 extension rule candidate clauses % 0.29/0.54 # 4 unit axiom clauses % 0.29/0.54 % 0.29/0.54 # Requested 8, 32 cores available to the main process. % 0.29/0.54 # There are not enough tableaux to fork, creating more from the initial 3 % 0.29/0.54 # Returning from population with 9 new_tableaux and 0 remaining starting tableaux. % 0.29/0.54 # We now have 9 tableaux to operate on % 0.39/0.65 # There were 1 total branch saturation attempts. % 0.39/0.65 # There were 0 of these attempts blocked. % 0.39/0.65 # There were 0 deferred branch saturation attempts. % 0.39/0.65 # There were 0 free duplicated saturations. % 0.39/0.65 # There were 1 total successful branch saturations. % 0.39/0.65 # There were 0 successful branch saturations in interreduction. % 0.39/0.65 # There were 0 successful branch saturations on the branch. % 0.39/0.65 # There were 1 successful branch saturations after the branch. % 0.39/0.65 # SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.39/0.65 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.39/0.65 # Begin clausification derivation % 0.39/0.65 % 0.39/0.65 # End clausification derivation % 0.39/0.65 # Begin listing active clauses obtained from FOF to CNF conversion % 0.39/0.65 cnf(i_0_3, negated_conjecture, (c_24__type__1___24t(esk1_0))). % 0.39/0.65 cnf(i_0_18, plain, (cDirectedSets_2eDirectedSet___24t(cI))). % 0.39/0.65 cnf(i_0_2, negated_conjecture, (~cDirectedSets_2efor__large_2eexists__arbitrarily__large___24a1(esk1_0))). % 0.39/0.65 cnf(i_0_1, negated_conjecture, (~cDirectedSets_2efor__large_2eeventually___24a1(happ(c_24__lam__34547,esk1_0)))). % 0.39/0.65 cnf(i_0_60, plain, (cType___24t(esk11_1(X1))|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_53, plain, (cDirectedSets_2eDS__set___24a1(X1)=esk11_1(X1)|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_72, plain, (cType___24t(esk14_1(X1))|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_62, plain, (~c_24__lam__34547___24a2(X1,X2)|~p(happ(X1,X2)))). % 0.39/0.65 cnf(i_0_25, plain, (cDirectedSets_2eDS__set___24t(cI,esk6_1(X1))|~cDirectedSets_2efor__large_2eeventually___24a1(X1))). % 0.39/0.65 cnf(i_0_13, plain, (c_24__type__1___24t(X1)|~cProp___24t(happ(X1,esk5_1(X1))))). % 0.39/0.65 cnf(i_0_17, plain, (t(X1,cDirectedSets_2eDS__set___24a1(X2))|~cDirectedSets_2eDS__set___24t(X2,X1))). % 0.39/0.65 cnf(i_0_9, plain, (cDirectedSets_2efor__large_2eexists__arbitrarily__large___24a1(X1)|cDirectedSets_2eDS__set___24t(cI,esk4_1(X1)))). % 0.39/0.65 cnf(i_0_14, plain, (c_24__type__1___24t(X1)|cDirectedSets_2eDS__set___24t(cI,esk5_1(X1)))). % 0.39/0.65 cnf(i_0_19, plain, (p(happ(happ(c_24__lam__34547,X1),X2))|~c_24__lam__34547___24a2(X1,X2))). % 0.39/0.65 cnf(i_0_20, plain, (c_24__lam__34547___24a2(X1,X2)|~p(happ(happ(c_24__lam__34547,X1),X2)))). % 0.39/0.65 cnf(i_0_21, plain, (cDirectedSets_2efor__large_2eeventually___24a1(X1)|~cDirectedSets_2eDS__set___24t(cI,X2)|~p(happ(X1,esk7_2(X1,X2))))). % 0.39/0.65 cnf(i_0_59, plain, (cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(esk11_1(X1),esk12_1(X1))|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_61, plain, (c_24__lam__34547___24a2(X1,X2)|p(happ(X1,X2)))). % 0.39/0.65 cnf(i_0_16, plain, (cDirectedSets_2eDS__set___24t(X1,X2)|~t(X2,cDirectedSets_2eDS__set___24a1(X1)))). % 0.39/0.65 cnf(i_0_64, plain, (X1=X2|cDirectedSets_2eBuild__DirectedSet___24a2(X3,X1)!=cDirectedSets_2eBuild__DirectedSet___24a2(X4,X2))). % 0.39/0.65 cnf(i_0_63, plain, (X1=X2|cDirectedSets_2eBuild__DirectedSet___24a2(X1,X3)!=cDirectedSets_2eBuild__DirectedSet___24a2(X2,X4))). % 0.39/0.65 cnf(i_0_54, plain, (cDirectedSets_2eBuild__DirectedSet___24a2(esk11_1(X1),esk12_1(X1))=X1|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_66, plain, (cDirectedSets_2eBuild__DirectedSet___24a2(esk14_1(X1),esk15_1(X1))=X1|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_15, plain, (cProp___24t(happ(X1,X2))|~c_24__type__1___24t(X1)|~cDirectedSets_2eDS__set___24t(cI,X2))). % 0.39/0.65 cnf(i_0_4, plain, (cDirectedSets_2efor__large_2eeventually___24a1(X1)|~c_24__type__1___24t(X2)|~c_24__type__1___24t(X1)|~cDirectedSets_2efor__large_2eeventually___24a1(X2)|~p(happ(X1,esk2_2(X2,X1))))). % 0.39/0.65 cnf(i_0_12, plain, (cDirectedSets_2eDS__set___24t(cI,esk3_2(X1,X2))|~cDirectedSets_2efor__large_2eexists__arbitrarily__large___24a1(X1)|~cDirectedSets_2eDS__set___24t(cI,X2))). % 0.39/0.65 cnf(i_0_10, plain, (p(happ(X1,esk3_2(X1,X2)))|~cDirectedSets_2efor__large_2eexists__arbitrarily__large___24a1(X1)|~cDirectedSets_2eDS__set___24t(cI,X2))). % 0.39/0.65 cnf(i_0_71, plain, (cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(esk14_1(X1),esk15_1(X1))|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_58, plain, (cCoq_2eRelations_2eRelation__Definitions_2epreorder___24a2(esk11_1(X1),esk12_1(X1))|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_135, plain, (c_24__type__169___24t(X1,X2)|~t(happ(X2,esk22_2(X1,X2)),X1))). % 0.39/0.65 cnf(i_0_70, plain, (cCoq_2eRelations_2eRelation__Definitions_2epreorder___24a2(esk14_1(X1),esk15_1(X1))|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_90, plain, (cCoq_2eClasses_2eRelationClasses_2eEquivalence___24a2(X1,X2)|~c_24__type__22___24t(X1,X2)|~cCoq_2eSetoids_2eSetoid_2eSetoid__Theory___24a2(X1,X2)|~cType___24t(X1))). % 0.39/0.65 cnf(i_0_137, plain, (t(happ(X1,X2),X3)|~c_24__type__169___24t(X3,X1)|~t(X2,X3))). % 0.39/0.65 cnf(i_0_140, plain, (c_24__type__780___24t(X1,X2)|t(esk23_2(X1,X2),X1))). % 0.39/0.65 cnf(i_0_23, plain, (cDirectedSets_2eDS__set___24t(cI,esk7_2(X1,X2))|cDirectedSets_2efor__large_2eeventually___24a1(X1)|~cDirectedSets_2eDS__set___24t(cI,X2))). % 0.39/0.65 cnf(i_0_6, plain, (cDirectedSets_2eDS__set___24t(cI,esk2_2(X1,X2))|cDirectedSets_2efor__large_2eeventually___24a1(X2)|~c_24__type__1___24t(X2)|~c_24__type__1___24t(X1)|~cDirectedSets_2efor__large_2eeventually___24a1(X1))). % 0.39/0.65 cnf(i_0_5, plain, (cDirectedSets_2efor__large_2eeventually___24a1(X1)|p(happ(X2,esk2_2(X2,X1)))|~c_24__type__1___24t(X1)|~c_24__type__1___24t(X2)|~cDirectedSets_2efor__large_2eeventually___24a1(X2))). % 0.39/0.65 cnf(i_0_139, plain, (c_24__type__780___24t(X1,X2)|t(esk24_2(X1,X2),X1))). % 0.39/0.65 cnf(i_0_136, plain, (c_24__type__169___24t(X1,X2)|t(esk22_2(X1,X2),X1))). % 0.39/0.65 cnf(i_0_31, plain, (c_24__type__22___24t(X1,X2)|t(esk9_2(X1,X2),X1))). % 0.39/0.65 cnf(i_0_8, plain, (cDirectedSets_2efor__large_2eexists__arbitrarily__large___24a1(X1)|~cDirectedSets_2eDS__ord___24a3(cI,esk4_1(X1),X2)|~cDirectedSets_2eDS__set___24t(cI,X2)|~p(happ(X1,X2)))). % 0.39/0.65 cnf(i_0_30, plain, (c_24__type__22___24t(X1,X2)|t(esk10_2(X1,X2),X1))). % 0.39/0.65 cnf(i_0_138, plain, (c_24__type__780___24t(X1,X2)|~t(happ(happ(X2,esk23_2(X1,X2)),esk24_2(X1,X2)),X1))). % 0.39/0.65 cnf(i_0_24, plain, (p(happ(X1,X2))|~cDirectedSets_2eDS__ord___24a3(cI,esk6_1(X1),X2)|~cDirectedSets_2eDS__set___24t(cI,X2)|~cDirectedSets_2efor__large_2eeventually___24a1(X1))). % 0.39/0.65 cnf(i_0_22, plain, (cDirectedSets_2eDS__ord___24a3(cI,X1,esk7_2(X2,X1))|cDirectedSets_2efor__large_2eeventually___24a1(X2)|~cDirectedSets_2eDS__set___24t(cI,X1))). % 0.39/0.65 cnf(i_0_29, plain, (c_24__type__22___24t(X1,X2)|~cProp___24t(happ(happ(X2,esk9_2(X1,X2)),esk10_2(X1,X2))))). % 0.39/0.65 cnf(i_0_11, plain, (cDirectedSets_2eDS__ord___24a3(cI,X1,esk3_2(X2,X1))|~cDirectedSets_2efor__large_2eexists__arbitrarily__large___24a1(X2)|~cDirectedSets_2eDS__set___24t(cI,X1))). % 0.39/0.65 cnf(i_0_28, plain, (cDirectedSets_2eDS__set___24t(X1,esk8_3(X1,X2,X3))|~cDirectedSets_2eDS__set___24t(X1,X3)|~cDirectedSets_2eDS__set___24t(X1,X2)|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_141, plain, (t(happ(happ(X1,X2),X3),X4)|~c_24__type__780___24t(X4,X1)|~t(X3,X4)|~t(X2,X4))). % 0.39/0.65 cnf(i_0_32, plain, (cProp___24t(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X1)|~t(X3,X4)|~t(X2,X4))). % 0.39/0.65 cnf(i_0_73, plain, (p(happ(happ(X1,X2),X2))|~cCoq_2eSetoids_2eSetoid_2eSetoid__Theory___24a2(X3,X1)|~cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X3,X1)|~t(X2,X3)|~cType___24t(X3))). % 0.39/0.65 cnf(i_0_57, plain, (t(esk13_3(X1,X2,X3),esk11_1(X1))|~cDirectedSets_2eDirectedSet___24t(X1)|~t(X3,esk11_1(X1))|~t(X2,esk11_1(X1)))). % 0.39/0.65 cnf(i_0_69, plain, (t(esk16_3(X1,X2,X3),esk14_1(X1))|~cDirectedSets_2eDirectedSet___24t(X1)|~t(X3,esk14_1(X1))|~t(X2,esk14_1(X1)))). % 0.39/0.65 cnf(i_0_26, plain, (cDirectedSets_2eDS__ord___24a3(X1,X2,esk8_3(X1,X3,X2))|~cDirectedSets_2eDS__set___24t(X1,X3)|~cDirectedSets_2eDS__set___24t(X1,X2)|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_27, plain, (cDirectedSets_2eDS__ord___24a3(X1,X2,esk8_3(X1,X2,X3))|~cDirectedSets_2eDS__set___24t(X1,X3)|~cDirectedSets_2eDS__set___24t(X1,X2)|~cDirectedSets_2eDirectedSet___24t(X1))). % 0.39/0.65 cnf(i_0_55, plain, (p(happ(happ(esk12_1(X1),X2),esk13_3(X1,X3,X2)))|~cDirectedSets_2eDirectedSet___24t(X1)|~t(X3,esk11_1(X1))|~t(X2,esk11_1(X1)))). % 0.39/0.65 cnf(i_0_56, plain, (p(happ(happ(esk12_1(X1),X2),esk13_3(X1,X2,X3)))|~cDirectedSets_2eDirectedSet___24t(X1)|~t(X3,esk11_1(X1))|~t(X2,esk11_1(X1)))). % 0.39/0.65 cnf(i_0_67, plain, (p(happ(happ(esk15_1(X1),X2),esk16_3(X1,X3,X2)))|~cDirectedSets_2eDirectedSet___24t(X1)|~t(X3,esk14_1(X1))|~t(X2,esk14_1(X1)))). % 0.39/0.65 cnf(i_0_68, plain, (p(happ(happ(esk15_1(X1),X2),esk16_3(X1,X2,X3)))|~cDirectedSets_2eDirectedSet___24t(X1)|~t(X3,esk14_1(X1))|~t(X2,esk14_1(X1)))). % 0.39/0.65 cnf(i_0_74, plain, (p(happ(happ(X1,X2),X3))|~cCoq_2eSetoids_2eSetoid_2eSetoid__Theory___24a2(X4,X1)|~cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X4,X1)|~t(X2,X4)|~t(X3,X4)|~cType___24t(X4)|~p(happ(happ(X1,X3),X2)))). % 0.39/0.65 cnf(i_0_75, plain, (p(happ(happ(X1,X2),X3))|~cCoq_2eSetoids_2eSetoid_2eSetoid__Theory___24a2(X4,X1)|~cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X4,X1)|~t(X3,X4)|~t(X5,X4)|~t(X2,X4)|~cType___24t(X4)|~p(happ(happ(X1,X5),X3))|~p(happ(happ(X1,X2),X5)))). % 0.39/0.65 cnf(i_0_89, plain, (cCoq_2eSetoids_2eSetoid_2eSetoid__Theory___24a2(X1,X2)|~c_24__type__22___24t(X1,X3)|~c_24__type__22___24t(X1,X4)|~c_24__type__22___24t(X1,X2)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X1,X5,X6,X7,X8,X9,X10,X2,X4,X3)|~c_24__type__169___24t(X1,X10)|~c_24__type__780___24t(X1,X9)|~c_24__type__780___24t(X1,X8)|~c_24__type__780___24t(X1,X7)|~t(X6,X1)|~t(X5,X1)|~cType___24t(X1))). % 0.39/0.65 cnf(i_0_111, plain, (~c_24__type__22___24t(X1,X2)|~c_24__type__22___24t(X1,X3)|~c_24__type__22___24t(X1,X4)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X1,X5,X6,X7,X8,X9,X10,X4,X3,X2)|~c_24__type__169___24t(X1,X10)|~c_24__type__780___24t(X1,X9)|~c_24__type__780___24t(X1,X8)|~c_24__type__780___24t(X1,X7)|~t(X6,X1)|~t(X5,X1)|~cType___24t(X1)|~p(happ(happ(X4,X5),X6)))). % 0.39/0.65 cnf(i_0_119, plain, (p(happ(happ(X1,X2),X2))|~c_24__type__22___24t(X3,X4)|~c_24__type__22___24t(X3,X1)|~c_24__type__22___24t(X3,X5)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X3,X6,X7,X8,X9,X10,X11,X5,X1,X4)|~c_24__type__169___24t(X3,X11)|~c_24__type__780___24t(X3,X10)|~c_24__type__780___24t(X3,X9)|~c_24__type__780___24t(X3,X8)|~t(X2,X3)|~t(X7,X3)|~t(X6,X3)|~cType___24t(X3))). % 0.39/0.65 cnf(i_0_107, plain, (~c_24__type__22___24t(X1,X2)|~c_24__type__22___24t(X1,X3)|~c_24__type__22___24t(X1,X4)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X1,X5,X6,X7,X8,X9,X10,X2,X3,X4)|~c_24__type__169___24t(X1,X10)|~c_24__type__780___24t(X1,X9)|~c_24__type__780___24t(X1,X8)|~c_24__type__780___24t(X1,X7)|~t(X6,X1)|~t(X5,X1)|~t(X11,X1)|~t(X12,X1)|~cType___24t(X1)|~p(happ(happ(X3,X11),X12))|~p(happ(happ(X4,X12),X11)))). % 0.39/0.65 cnf(i_0_93, plain, (p(happ(happ(X1,X2),X3))|p(happ(happ(X4,X3),X2))|~c_24__type__22___24t(X5,X4)|~c_24__type__22___24t(X5,X1)|~c_24__type__22___24t(X5,X6)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X5,X7,X8,X9,X10,X11,X12,X6,X1,X4)|~c_24__type__169___24t(X5,X12)|~c_24__type__780___24t(X5,X11)|~c_24__type__780___24t(X5,X10)|~c_24__type__780___24t(X5,X9)|~t(X3,X5)|~t(X2,X5)|~t(X8,X5)|~t(X7,X5)|~cType___24t(X5))). % 0.39/0.65 cnf(i_0_100, plain, (~c_24__type__22___24t(X1,X2)|~c_24__type__22___24t(X1,X3)|~c_24__type__22___24t(X1,X4)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X1,X5,X6,X7,X8,X9,X10,X4,X2,X3)|~c_24__type__169___24t(X1,X10)|~c_24__type__780___24t(X1,X9)|~c_24__type__780___24t(X1,X8)|~c_24__type__780___24t(X1,X7)|~t(X6,X1)|~t(X5,X1)|~t(X11,X1)|~t(X12,X1)|~cType___24t(X1)|~p(happ(happ(X3,X12),X11))|~p(happ(happ(X4,X12),X11)))). % 0.39/0.65 cnf(i_0_112, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~c_24__type__22___24t(X4,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X1,X6,X5)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X11)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~t(X3,X4)|~t(X2,X4)|~t(X8,X4)|~t(X7,X4)|~cType___24t(X4)|~p(happ(happ(X1,X3),X2)))). % 0.39/0.65 cnf(i_0_101, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~c_24__type__22___24t(X4,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X5,X1,X6)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X11)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~t(X8,X4)|~t(X7,X4)|~t(X3,X4)|~t(X2,X4)|~cType___24t(X4)|~p(happ(happ(X6,X2),X3)))). % 0.39/0.65 cnf(i_0_103, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~c_24__type__22___24t(X4,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X6,X5,X1)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~c_24__type__780___24t(X4,X11)|~t(X8,X4)|~t(X2,X4)|~t(X3,X4)|~t(X7,X4)|~cType___24t(X4)|~p(happ(happ(X1,X7),happ(happ(X11,X3),X2))))). % 0.39/0.65 cnf(i_0_113, plain, (p(happ(happ(X1,happ(happ(X2,X3),X4)),happ(happ(X2,X4),X3)))|~c_24__type__22___24t(X5,X6)|~c_24__type__22___24t(X5,X7)|~c_24__type__22___24t(X5,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X5,X8,X9,X10,X2,X11,X12,X1,X7,X6)|~c_24__type__169___24t(X5,X12)|~c_24__type__780___24t(X5,X11)|~c_24__type__780___24t(X5,X2)|~c_24__type__780___24t(X5,X10)|~t(X4,X5)|~t(X3,X5)|~t(X9,X5)|~t(X8,X5)|~cType___24t(X5))). % 0.39/0.65 cnf(i_0_94, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~c_24__type__22___24t(X4,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X6,X1,X5)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~c_24__type__780___24t(X4,X11)|~t(X8,X4)|~t(X2,X4)|~t(X3,X4)|~t(X7,X4)|~cType___24t(X4)|~p(happ(happ(X1,X7),happ(happ(X11,X3),X2))))). % 0.39/0.65 cnf(i_0_110, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~c_24__type__22___24t(X4,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X1,X6,X5)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~c_24__type__780___24t(X4,X11)|~t(X8,X4)|~t(X7,X4)|~t(X3,X4)|~t(X2,X4)|~cType___24t(X4)|~p(happ(happ(X1,happ(happ(X11,X2),X3)),X7)))). % 0.39/0.65 cnf(i_0_104, plain, (p(happ(happ(X1,X2),happ(happ(X3,X4),X5)))|~c_24__type__22___24t(X6,X7)|~c_24__type__22___24t(X6,X8)|~c_24__type__22___24t(X6,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X6,X2,X9,X10,X11,X3,X12,X8,X7,X1)|~c_24__type__169___24t(X6,X12)|~c_24__type__780___24t(X6,X11)|~c_24__type__780___24t(X6,X10)|~c_24__type__780___24t(X6,X3)|~t(X9,X6)|~t(X2,X6)|~t(X4,X6)|~t(X5,X6)|~cType___24t(X6)|~p(happ(happ(X1,X5),X4)))). % 0.39/0.65 cnf(i_0_95, plain, (p(happ(happ(X1,X2),happ(happ(X3,X4),X5)))|~c_24__type__22___24t(X6,X7)|~c_24__type__22___24t(X6,X8)|~c_24__type__22___24t(X6,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X6,X2,X9,X10,X11,X3,X12,X8,X1,X7)|~c_24__type__169___24t(X6,X12)|~c_24__type__780___24t(X6,X11)|~c_24__type__780___24t(X6,X10)|~c_24__type__780___24t(X6,X3)|~t(X9,X6)|~t(X2,X6)|~t(X4,X6)|~t(X5,X6)|~cType___24t(X6)|~p(happ(happ(X1,X5),X4)))). % 0.39/0.65 cnf(i_0_108, plain, (p(happ(happ(X1,X2),X3))|p(happ(happ(X4,X2),X3))|p(happ(happ(X4,X3),X2))|~c_24__type__22___24t(X5,X4)|~c_24__type__22___24t(X5,X6)|~c_24__type__22___24t(X5,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X5,X7,X8,X9,X10,X11,X12,X1,X6,X4)|~c_24__type__169___24t(X5,X12)|~c_24__type__780___24t(X5,X11)|~c_24__type__780___24t(X5,X10)|~c_24__type__780___24t(X5,X9)|~t(X3,X5)|~t(X2,X5)|~t(X8,X5)|~t(X7,X5)|~cType___24t(X5))). % 0.39/0.65 cnf(i_0_130, plain, (p(happ(happ(X1,happ(X2,X3)),happ(X2,X4)))|~c_24__type__22___24t(X5,X6)|~c_24__type__22___24t(X5,X7)|~c_24__type__22___24t(X5,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X5,X8,X9,X10,X11,X12,X2,X1,X7,X6)|~c_24__type__169___24t(X5,X2)|~c_24__type__780___24t(X5,X12)|~c_24__type__780___24t(X5,X11)|~c_24__type__780___24t(X5,X10)|~t(X4,X5)|~t(X3,X5)|~t(X9,X5)|~t(X8,X5)|~cType___24t(X5)|~p(happ(happ(X1,X3),X4)))). % 0.39/0.65 cnf(i_0_118, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~c_24__type__22___24t(X4,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X1,X6,X5)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X11)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~t(X3,X4)|~t(X2,X4)|~t(X8,X4)|~t(X7,X4)|~cType___24t(X4)|~p(happ(happ(X6,X3),X2))|~p(happ(happ(X6,X2),X3)))). % 0.39/0.65 cnf(i_0_109, plain, (p(happ(happ(X1,happ(happ(X2,X3),X4)),X5))|~c_24__type__22___24t(X6,X7)|~c_24__type__22___24t(X6,X8)|~c_24__type__22___24t(X6,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X6,X5,X9,X10,X11,X2,X12,X1,X8,X7)|~c_24__type__169___24t(X6,X12)|~c_24__type__780___24t(X6,X11)|~c_24__type__780___24t(X6,X10)|~c_24__type__780___24t(X6,X2)|~t(X9,X6)|~t(X5,X6)|~t(X4,X6)|~t(X3,X6)|~cType___24t(X6)|~p(happ(happ(X1,X3),X4)))). % 0.39/0.65 cnf(i_0_96, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X1)|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X6,X5,X1)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X11)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~t(X3,X4)|~t(X13,X4)|~t(X2,X4)|~t(X8,X4)|~t(X7,X4)|~cType___24t(X4)|~p(happ(happ(X1,X13),X3))|~p(happ(happ(X5,X2),X13)))). % 0.39/0.65 cnf(i_0_102, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X1)|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X6,X5,X1)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X11)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~t(X3,X4)|~t(X13,X4)|~t(X2,X4)|~t(X8,X4)|~t(X7,X4)|~cType___24t(X4)|~p(happ(happ(X1,X2),X13))|~p(happ(happ(X5,X13),X3)))). % 0.39/0.65 cnf(i_0_99, plain, (p(happ(happ(X1,X2),X3))|p(happ(happ(X4,X2),X3))|~c_24__type__22___24t(X5,X4)|~c_24__type__22___24t(X5,X1)|~c_24__type__22___24t(X5,X6)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X5,X7,X8,X9,X10,X11,X12,X1,X6,X4)|~c_24__type__169___24t(X5,X12)|~c_24__type__780___24t(X5,X11)|~c_24__type__780___24t(X5,X10)|~c_24__type__780___24t(X5,X9)|~t(X8,X5)|~t(X7,X5)|~t(X3,X5)|~t(X2,X5)|~cType___24t(X5)|~p(happ(happ(X6,X2),X3)))). % 0.39/0.65 cnf(i_0_120, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X1)|~c_24__type__22___24t(X4,X6)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X6,X1,X5)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X11)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~t(X3,X4)|~t(X13,X4)|~t(X2,X4)|~t(X8,X4)|~t(X7,X4)|~cType___24t(X4)|~p(happ(happ(X1,X13),X3))|~p(happ(happ(X1,X2),X13)))). % 0.39/0.65 cnf(i_0_114, plain, (p(happ(happ(X1,X2),happ(happ(X3,X4),X5)))|~c_24__type__22___24t(X6,X1)|~c_24__type__22___24t(X6,X7)|~c_24__type__22___24t(X6,X8)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X6,X2,X9,X10,X3,X11,X12,X8,X7,X1)|~c_24__type__169___24t(X6,X12)|~c_24__type__780___24t(X6,X11)|~c_24__type__780___24t(X6,X3)|~c_24__type__780___24t(X6,X10)|~t(X5,X6)|~t(X4,X6)|~t(X9,X6)|~t(X2,X6)|~cType___24t(X6)|~p(happ(happ(X1,X5),X2))|~p(happ(happ(X1,X4),X2)))). % 0.39/0.65 cnf(i_0_117, plain, (p(happ(happ(X1,X2),happ(happ(X3,X4),X5)))|~c_24__type__22___24t(X6,X1)|~c_24__type__22___24t(X6,X7)|~c_24__type__22___24t(X6,X8)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X6,X2,X9,X10,X3,X11,X12,X8,X7,X1)|~c_24__type__169___24t(X6,X12)|~c_24__type__780___24t(X6,X11)|~c_24__type__780___24t(X6,X3)|~c_24__type__780___24t(X6,X10)|~t(X5,X6)|~t(X4,X6)|~t(X9,X6)|~t(X2,X6)|~cType___24t(X6)|~p(happ(happ(X1,X2),X5))|~p(happ(happ(X1,X2),X4)))). % 0.39/0.65 cnf(i_0_116, plain, (p(happ(happ(X1,happ(happ(X2,X3),X4)),X5))|~c_24__type__22___24t(X6,X1)|~c_24__type__22___24t(X6,X7)|~c_24__type__22___24t(X6,X8)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X6,X5,X9,X10,X2,X11,X12,X8,X7,X1)|~c_24__type__169___24t(X6,X12)|~c_24__type__780___24t(X6,X11)|~c_24__type__780___24t(X6,X2)|~c_24__type__780___24t(X6,X10)|~t(X4,X6)|~t(X3,X6)|~t(X9,X6)|~t(X5,X6)|~cType___24t(X6)|~p(happ(happ(X1,X4),X5))|~p(happ(happ(X1,X5),X3)))). % 0.39/0.65 cnf(i_0_115, plain, (p(happ(happ(X1,X2),X3))|p(happ(happ(X1,X4),X3))|~c_24__type__22___24t(X5,X6)|~c_24__type__22___24t(X5,X7)|~c_24__type__22___24t(X5,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X5,X3,X8,X9,X10,X11,X12,X1,X7,X6)|~c_24__type__169___24t(X5,X12)|~c_24__type__780___24t(X5,X11)|~c_24__type__780___24t(X5,X10)|~c_24__type__780___24t(X5,X9)|~t(X4,X5)|~t(X2,X5)|~t(X8,X5)|~t(X3,X5)|~cType___24t(X5)|~p(happ(happ(X1,happ(happ(X10,X2),X4)),X3)))). % 0.39/0.65 cnf(i_0_127, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~c_24__type__22___24t(X4,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X6,X5,X1)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X11)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~t(X8,X4)|~t(X7,X4)|~t(X3,X4)|~t(X2,X4)|~t(X13,X4)|~t(X14,X4)|~cType___24t(X4)|~p(happ(happ(X6,X3),X13))|~p(happ(happ(X6,X2),X14))|~p(happ(happ(X1,X14),X13)))). % 0.39/0.65 cnf(i_0_121, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~c_24__type__22___24t(X4,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X6,X1,X5)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X11)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~t(X8,X4)|~t(X7,X4)|~t(X3,X4)|~t(X2,X4)|~t(X13,X4)|~t(X14,X4)|~cType___24t(X4)|~p(happ(happ(X6,X3),X13))|~p(happ(happ(X6,X2),X14))|~p(happ(happ(X1,X14),X13)))). % 0.39/0.65 cnf(i_0_131, plain, (p(happ(happ(X1,happ(happ(X2,X3),X4)),happ(happ(X2,X3),X5)))|~c_24__type__22___24t(X6,X7)|~c_24__type__22___24t(X6,X1)|~c_24__type__22___24t(X6,X8)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X6,X9,X10,X2,X11,X12,X13,X8,X1,X7)|~c_24__type__169___24t(X6,X13)|~c_24__type__780___24t(X6,X12)|~c_24__type__780___24t(X6,X11)|~c_24__type__780___24t(X6,X2)|~t(X3,X6)|~t(X5,X6)|~t(X4,X6)|~t(X10,X6)|~t(X9,X6)|~cType___24t(X6)|~p(happ(happ(X1,X4),X5)))). % 0.39/0.65 cnf(i_0_128, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~c_24__type__22___24t(X4,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X6,X5,X1)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X11)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~t(X8,X4)|~t(X7,X4)|~t(X3,X4)|~t(X2,X4)|~t(X13,X4)|~t(X14,X4)|~cType___24t(X4)|~p(happ(happ(X6,X13),X3))|~p(happ(happ(X6,X14),X2))|~p(happ(happ(X1,X14),X13)))). % 0.39/0.65 cnf(i_0_122, plain, (p(happ(happ(X1,X2),X3))|~c_24__type__22___24t(X4,X5)|~c_24__type__22___24t(X4,X6)|~c_24__type__22___24t(X4,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X4,X7,X8,X9,X10,X11,X12,X6,X1,X5)|~c_24__type__169___24t(X4,X12)|~c_24__type__780___24t(X4,X11)|~c_24__type__780___24t(X4,X10)|~c_24__type__780___24t(X4,X9)|~t(X8,X4)|~t(X7,X4)|~t(X3,X4)|~t(X2,X4)|~t(X13,X4)|~t(X14,X4)|~cType___24t(X4)|~p(happ(happ(X6,X13),X3))|~p(happ(happ(X6,X14),X2))|~p(happ(happ(X1,X14),X13)))). % 0.39/0.65 cnf(i_0_134, plain, (p(happ(happ(X1,happ(happ(X2,X3),X4)),happ(happ(X2,X5),X6)))|~c_24__type__22___24t(X7,X8)|~c_24__type__22___24t(X7,X9)|~c_24__type__22___24t(X7,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X7,X10,X11,X12,X2,X13,X14,X1,X9,X8)|~c_24__type__169___24t(X7,X14)|~c_24__type__780___24t(X7,X13)|~c_24__type__780___24t(X7,X2)|~c_24__type__780___24t(X7,X12)|~t(X6,X7)|~t(X4,X7)|~t(X5,X7)|~t(X3,X7)|~t(X11,X7)|~t(X10,X7)|~cType___24t(X7)|~p(happ(happ(X1,X4),X6))|~p(happ(happ(X1,X3),X5)))). % 0.39/0.65 cnf(i_0_132, plain, (p(happ(happ(X1,happ(happ(X2,X3),X4)),happ(happ(X2,X5),X6)))|~c_24__type__22___24t(X7,X8)|~c_24__type__22___24t(X7,X9)|~c_24__type__22___24t(X7,X1)|~cCoq_2emicromega_2eOrderedRing_2eSOR___24a10(X7,X10,X11,X2,X12,X13,X14,X1,X9,X8)|~c_24__type__169___24t(X7,X14)|~c_24__type__780___24t(X7,X13)|~c_24__type__780___24t(X7,X12)|~c_24__type__780___24t(X7,X2)|~t(X6,X7)|~t(X4,X7)|~t(X5,X7)|~t(X3,X7)|~t(X11,X7)|~t(X10,X7)|~cType___24t(X7)|~p(happ(happ(X1,X4),X6))|~p(happ(happ(X1,X3),X5)))). % 0.39/0.65 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 0.39/0.65 # Begin printing tableau % 0.39/0.65 # Found 4 steps % 0.39/0.65 cnf(i_0_2, negated_conjecture, (~cDirectedSets_2efor__large_2eexists__arbitrarily__large___24a1(esk1_0)), inference(start_rule)). % 0.39/0.65 cnf(i_0_143, plain, (~cDirectedSets_2efor__large_2eexists__arbitrarily__large___24a1(esk1_0)), inference(extension_rule, [i_0_9])). % 0.39/0.65 cnf(i_0_856, plain, (cDirectedSets_2eDS__set___24t(cI,esk4_1(esk1_0))), inference(extension_rule, [i_0_17])). % 0.39/0.65 cnf(i_0_1549, plain, (t(esk4_1(esk1_0),cDirectedSets_2eDS__set___24a1(cI))), inference(etableau_closure_rule, [i_0_1549, ...])). % 0.39/0.65 # End printing tableau % 0.39/0.65 # SZS output end % 0.39/0.65 # Branches closed with saturation will be marked with an "s" % 0.39/0.66 # Child (25338) has found a proof. % 0.39/0.66 % 0.39/0.66 # Proof search is over... % 0.39/0.66 # Freeing feature tree %------------------------------------------------------------------------------