%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU139+2 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n028.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 : Mon Jun 24 15:01:16 EDT 2024 % Result : Theorem 0.56s 0.69s % Output : CNFRefutation 0.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SEU139+2 : TPTP v8.2.0. Released v3.3.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n028.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 21 11:50:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.21/0.58 start to proof:theBenchmark % 0.56/0.67 %------------------------------------------- % 0.56/0.67 % File :CSE---1.7 % 0.56/0.67 % Problem :theBenchmark % 0.56/0.67 % Transform :cnf % 0.56/0.67 % Format :tptp:raw % 0.56/0.67 % Command :java -jar mcs_scs.jar %d %s % 0.56/0.67 % 0.56/0.67 % Result :Theorem 0.000000s % 0.56/0.67 % Output :CNFRefutation 0.000000s % 0.56/0.67 %------------------------------------------- % 0.56/0.67 %------------------------------------------------------------------------------ % 0.56/0.67 % File : SEU139+2 : TPTP v8.2.0. Released v3.3.0. % 0.56/0.67 % Domain : Set theory % 0.56/0.67 % Problem : MPTP chainy problem t60_xboole_1 % 0.56/0.67 % Version : [Urb07] axioms : Especial. % 0.56/0.67 % English : % 0.56/0.67 % 0.56/0.67 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.56/0.67 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.56/0.67 % Source : [Urb07] % 0.56/0.67 % Names : chainy-t60_xboole_1 [Urb07] % 0.56/0.67 % 0.56/0.67 % Status : Theorem % 0.56/0.67 % Rating : 0.03 v8.1.0, 0.00 v6.3.0, 0.04 v6.2.0, 0.12 v6.1.0, 0.10 v6.0.0, 0.13 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.19 v5.2.0, 0.00 v5.0.0, 0.12 v4.1.0, 0.09 v4.0.1, 0.13 v4.0.0, 0.17 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0, 0.16 v3.3.0 % 0.56/0.67 % Syntax : Number of formulae : 55 ( 24 unt; 0 def) % 0.56/0.67 % Number of atoms : 106 ( 27 equ) % 0.56/0.67 % Maximal formula atoms : 6 ( 1 avg) % 0.56/0.67 % Number of connectives : 74 ( 23 ~; 1 |; 19 &) % 0.56/0.67 % ( 14 <=>; 17 =>; 0 <=; 0 <~>) % 0.56/0.67 % Maximal formula depth : 9 ( 4 avg) % 0.56/0.67 % Maximal term depth : 3 ( 1 avg) % 0.56/0.67 % Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty) % 0.56/0.67 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 0.56/0.67 % Number of variables : 108 ( 104 !; 4 ?) % 0.56/0.67 % SPC : FOF_THM_RFO_SEQ % 0.56/0.67 % 0.56/0.67 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.56/0.67 % library, www.mizar.org % 0.56/0.67 %------------------------------------------------------------------------------ % 0.56/0.67 fof(antisymmetry_r2_hidden,axiom, % 0.56/0.67 ! [A,B] : % 0.56/0.67 ( in(A,B) % 0.56/0.67 => ~ in(B,A) ) ). % 0.56/0.67 % 0.56/0.67 fof(antisymmetry_r2_xboole_0,axiom, % 0.56/0.67 ! [A,B] : % 0.56/0.67 ( proper_subset(A,B) % 0.56/0.68 => ~ proper_subset(B,A) ) ). % 0.56/0.68 % 0.56/0.68 fof(commutativity_k2_xboole_0,axiom, % 0.56/0.68 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 0.56/0.68 % 0.56/0.68 fof(commutativity_k3_xboole_0,axiom, % 0.56/0.68 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 0.56/0.68 % 0.56/0.68 fof(d10_xboole_0,axiom, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( A = B % 0.56/0.68 <=> ( subset(A,B) % 0.56/0.68 & subset(B,A) ) ) ). % 0.56/0.68 % 0.56/0.68 fof(d1_xboole_0,axiom, % 0.56/0.68 ! [A] : % 0.56/0.68 ( A = empty_set % 0.56/0.68 <=> ! [B] : ~ in(B,A) ) ). % 0.56/0.68 % 0.56/0.68 fof(d2_xboole_0,axiom, % 0.56/0.68 ! [A,B,C] : % 0.56/0.68 ( C = set_union2(A,B) % 0.56/0.68 <=> ! [D] : % 0.56/0.68 ( in(D,C) % 0.56/0.68 <=> ( in(D,A) % 0.56/0.68 | in(D,B) ) ) ) ). % 0.56/0.68 % 0.56/0.68 fof(d3_tarski,axiom, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( subset(A,B) % 0.56/0.68 <=> ! [C] : % 0.56/0.68 ( in(C,A) % 0.56/0.68 => in(C,B) ) ) ). % 0.56/0.68 % 0.56/0.68 fof(d3_xboole_0,axiom, % 0.56/0.68 ! [A,B,C] : % 0.56/0.68 ( C = set_intersection2(A,B) % 0.56/0.68 <=> ! [D] : % 0.56/0.68 ( in(D,C) % 0.56/0.68 <=> ( in(D,A) % 0.56/0.68 & in(D,B) ) ) ) ). % 0.56/0.68 % 0.56/0.68 fof(d4_xboole_0,axiom, % 0.56/0.68 ! [A,B,C] : % 0.56/0.68 ( C = set_difference(A,B) % 0.56/0.68 <=> ! [D] : % 0.56/0.68 ( in(D,C) % 0.56/0.68 <=> ( in(D,A) % 0.56/0.68 & ~ in(D,B) ) ) ) ). % 0.56/0.68 % 0.56/0.68 fof(d7_xboole_0,axiom, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( disjoint(A,B) % 0.56/0.68 <=> set_intersection2(A,B) = empty_set ) ). % 0.56/0.68 % 0.56/0.68 fof(d8_xboole_0,axiom, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( proper_subset(A,B) % 0.56/0.68 <=> ( subset(A,B) % 0.56/0.68 & A != B ) ) ). % 0.56/0.68 % 0.56/0.68 fof(dt_k1_xboole_0,axiom, % 0.56/0.68 $true ). % 0.56/0.68 % 0.56/0.68 fof(dt_k2_xboole_0,axiom, % 0.56/0.68 $true ). % 0.56/0.68 % 0.56/0.68 fof(dt_k3_xboole_0,axiom, % 0.56/0.68 $true ). % 0.56/0.68 % 0.56/0.68 fof(dt_k4_xboole_0,axiom, % 0.56/0.68 $true ). % 0.56/0.68 % 0.56/0.68 fof(fc1_xboole_0,axiom, % 0.56/0.68 empty(empty_set) ). % 0.56/0.68 % 0.56/0.68 fof(fc2_xboole_0,axiom, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( ~ empty(A) % 0.56/0.68 => ~ empty(set_union2(A,B)) ) ). % 0.56/0.68 % 0.56/0.68 fof(fc3_xboole_0,axiom, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( ~ empty(A) % 0.56/0.68 => ~ empty(set_union2(B,A)) ) ). % 0.56/0.68 % 0.56/0.68 fof(idempotence_k2_xboole_0,axiom, % 0.56/0.68 ! [A,B] : set_union2(A,A) = A ). % 0.56/0.68 % 0.56/0.68 fof(idempotence_k3_xboole_0,axiom, % 0.56/0.68 ! [A,B] : set_intersection2(A,A) = A ). % 0.56/0.68 % 0.56/0.68 fof(irreflexivity_r2_xboole_0,axiom, % 0.56/0.68 ! [A,B] : ~ proper_subset(A,A) ). % 0.56/0.68 % 0.56/0.68 fof(l32_xboole_1,lemma, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( set_difference(A,B) = empty_set % 0.56/0.68 <=> subset(A,B) ) ). % 0.56/0.68 % 0.56/0.68 fof(rc1_xboole_0,axiom, % 0.56/0.68 ? [A] : empty(A) ). % 0.56/0.68 % 0.56/0.68 fof(rc2_xboole_0,axiom, % 0.56/0.68 ? [A] : ~ empty(A) ). % 0.56/0.68 % 0.56/0.68 fof(reflexivity_r1_tarski,axiom, % 0.56/0.68 ! [A,B] : subset(A,A) ). % 0.56/0.68 % 0.56/0.68 fof(symmetry_r1_xboole_0,axiom, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( disjoint(A,B) % 0.56/0.68 => disjoint(B,A) ) ). % 0.56/0.68 % 0.56/0.68 fof(t12_xboole_1,lemma, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( subset(A,B) % 0.56/0.68 => set_union2(A,B) = B ) ). % 0.56/0.68 % 0.56/0.68 fof(t17_xboole_1,lemma, % 0.56/0.68 ! [A,B] : subset(set_intersection2(A,B),A) ). % 0.56/0.68 % 0.56/0.68 fof(t19_xboole_1,lemma, % 0.56/0.68 ! [A,B,C] : % 0.56/0.68 ( ( subset(A,B) % 0.56/0.68 & subset(A,C) ) % 0.56/0.68 => subset(A,set_intersection2(B,C)) ) ). % 0.56/0.68 % 0.56/0.68 fof(t1_boole,axiom, % 0.56/0.68 ! [A] : set_union2(A,empty_set) = A ). % 0.56/0.68 % 0.56/0.68 fof(t1_xboole_1,lemma, % 0.56/0.68 ! [A,B,C] : % 0.56/0.68 ( ( subset(A,B) % 0.56/0.68 & subset(B,C) ) % 0.56/0.68 => subset(A,C) ) ). % 0.56/0.68 % 0.56/0.68 fof(t26_xboole_1,lemma, % 0.56/0.68 ! [A,B,C] : % 0.56/0.68 ( subset(A,B) % 0.56/0.68 => subset(set_intersection2(A,C),set_intersection2(B,C)) ) ). % 0.56/0.68 % 0.56/0.68 fof(t28_xboole_1,lemma, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( subset(A,B) % 0.56/0.68 => set_intersection2(A,B) = A ) ). % 0.56/0.68 % 0.56/0.68 fof(t2_boole,axiom, % 0.56/0.68 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 0.56/0.68 % 0.56/0.68 fof(t2_tarski,axiom, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( ! [C] : % 0.56/0.68 ( in(C,A) % 0.56/0.68 <=> in(C,B) ) % 0.56/0.68 => A = B ) ). % 0.56/0.68 % 0.56/0.68 fof(t2_xboole_1,lemma, % 0.56/0.68 ! [A] : subset(empty_set,A) ). % 0.56/0.68 % 0.56/0.68 fof(t33_xboole_1,lemma, % 0.56/0.68 ! [A,B,C] : % 0.56/0.68 ( subset(A,B) % 0.56/0.68 => subset(set_difference(A,C),set_difference(B,C)) ) ). % 0.56/0.68 % 0.56/0.68 fof(t36_xboole_1,lemma, % 0.56/0.68 ! [A,B] : subset(set_difference(A,B),A) ). % 0.56/0.68 % 0.56/0.68 fof(t37_xboole_1,lemma, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( set_difference(A,B) = empty_set % 0.56/0.68 <=> subset(A,B) ) ). % 0.56/0.68 % 0.56/0.68 fof(t39_xboole_1,lemma, % 0.56/0.68 ! [A,B] : set_union2(A,set_difference(B,A)) = set_union2(A,B) ). % 0.56/0.68 % 0.56/0.68 fof(t3_boole,axiom, % 0.56/0.68 ! [A] : set_difference(A,empty_set) = A ). % 0.56/0.68 % 0.56/0.68 fof(t3_xboole_0,lemma, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( ~ ( ~ disjoint(A,B) % 0.56/0.68 & ! [C] : % 0.56/0.68 ~ ( in(C,A) % 0.56/0.68 & in(C,B) ) ) % 0.56/0.68 & ~ ( ? [C] : % 0.56/0.68 ( in(C,A) % 0.56/0.68 & in(C,B) ) % 0.56/0.68 & disjoint(A,B) ) ) ). % 0.56/0.68 % 0.56/0.68 fof(t3_xboole_1,lemma, % 0.56/0.68 ! [A] : % 0.56/0.68 ( subset(A,empty_set) % 0.56/0.68 => A = empty_set ) ). % 0.56/0.68 % 0.56/0.68 fof(t40_xboole_1,lemma, % 0.56/0.68 ! [A,B] : set_difference(set_union2(A,B),B) = set_difference(A,B) ). % 0.56/0.68 % 0.56/0.68 fof(t45_xboole_1,lemma, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( subset(A,B) % 0.56/0.68 => B = set_union2(A,set_difference(B,A)) ) ). % 0.56/0.68 % 0.56/0.68 fof(t48_xboole_1,lemma, % 0.56/0.68 ! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B) ). % 0.56/0.68 % 0.56/0.68 fof(t4_boole,axiom, % 0.56/0.68 ! [A] : set_difference(empty_set,A) = empty_set ). % 0.56/0.68 % 0.56/0.68 fof(t4_xboole_0,lemma, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ( ~ ( ~ disjoint(A,B) % 0.56/0.68 & ! [C] : ~ in(C,set_intersection2(A,B)) ) % 0.56/0.68 & ~ ( ? [C] : in(C,set_intersection2(A,B)) % 0.56/0.68 & disjoint(A,B) ) ) ). % 0.56/0.68 % 0.56/0.68 fof(t60_xboole_1,conjecture, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ~ ( subset(A,B) % 0.56/0.68 & proper_subset(B,A) ) ). % 0.56/0.68 % 0.56/0.68 fof(t6_boole,axiom, % 0.56/0.68 ! [A] : % 0.56/0.68 ( empty(A) % 0.56/0.68 => A = empty_set ) ). % 0.56/0.68 % 0.56/0.68 fof(t7_boole,axiom, % 0.56/0.68 ! [A,B] : % 0.56/0.68 ~ ( in(A,B) % 0.56/0.68 & empty(B) ) ). % 0.56/0.68 % 0.56/0.68 fof(t7_xboole_1,lemma, % 0.56/0.68 ! [A,B] : subset(A,set_union2(A,B)) ). % 0.56/0.68 % 0.56/0.68 fof(t8_boole,axiom, % 0.56/0.68 ! [A,B] : % 0.56/0.69 ~ ( empty(A) % 0.56/0.69 & A != B % 0.56/0.69 & empty(B) ) ). % 0.56/0.69 % 0.56/0.69 fof(t8_xboole_1,lemma, % 0.56/0.69 ! [A,B,C] : % 0.56/0.69 ( ( subset(A,B) % 0.56/0.69 & subset(C,B) ) % 0.56/0.69 => subset(set_union2(A,C),B) ) ). % 0.56/0.69 % 0.56/0.69 %------------------------------------------------------------------------------ % 0.56/0.69 %------------------------------------------- % 0.56/0.69 % Proof found % 0.56/0.69 % SZS status Theorem for theBenchmark % 0.56/0.69 % SZS output start Proof % 0.56/0.69 %ClaNum:114(EqnAxiom:34) % 0.56/0.69 %VarNum:413(SingletonVarNum:161) % 0.56/0.69 %MaxLitNum:4 % 0.56/0.69 %MaxfuncDepth:2 % 0.56/0.69 %SharedTerms:10 % 0.56/0.69 %goalClause: 37 38 % 0.56/0.69 %singleGoalClaCount:2 % 0.56/0.69 [35]P1(a1) % 0.56/0.69 [36]P1(a2) % 0.56/0.69 [37]P3(a3,a4) % 0.56/0.69 [38]P5(a4,a3) % 0.56/0.69 [54]~P1(a12) % 0.56/0.69 [40]P5(a1,x401) % 0.56/0.69 [43]P5(x431,x431) % 0.56/0.69 [55]~P3(x551,x551) % 0.56/0.69 [39]E(f11(a1,x391),a1) % 0.56/0.69 [41]E(f15(x411,a1),x411) % 0.56/0.69 [42]E(f11(x421,a1),x421) % 0.56/0.69 [44]E(f15(x441,x441),x441) % 0.56/0.69 [46]E(f11(x461,f11(x461,a1)),a1) % 0.56/0.69 [49]E(f11(x491,f11(x491,x491)),x491) % 0.56/0.69 [45]E(f15(x451,x452),f15(x452,x451)) % 0.56/0.69 [47]P5(x471,f15(x471,x472)) % 0.56/0.69 [48]P5(f11(x481,x482),x481) % 0.56/0.69 [50]E(f15(x501,f11(x502,x501)),f15(x501,x502)) % 0.56/0.69 [51]E(f11(f15(x511,x512),x512),f11(x511,x512)) % 0.56/0.69 [52]E(f11(x521,f11(x521,x522)),f11(x522,f11(x522,x521))) % 0.56/0.69 [56]~P1(x561)+E(x561,a1) % 0.56/0.69 [60]~P5(x601,a1)+E(x601,a1) % 0.56/0.69 [61]P4(f6(x611),x611)+E(x611,a1) % 0.56/0.69 [59]~E(x591,x592)+P5(x591,x592) % 0.56/0.69 [62]~P4(x622,x621)+~E(x621,a1) % 0.56/0.69 [63]~P3(x631,x632)+~E(x631,x632) % 0.56/0.69 [64]~P1(x641)+~P4(x642,x641) % 0.56/0.69 [69]~P3(x691,x692)+P5(x691,x692) % 0.56/0.69 [70]~P2(x702,x701)+P2(x701,x702) % 0.56/0.69 [73]~P4(x732,x731)+~P4(x731,x732) % 0.56/0.69 [74]~P3(x742,x741)+~P3(x741,x742) % 0.56/0.69 [66]~P5(x661,x662)+E(f11(x661,x662),a1) % 0.56/0.69 [68]P5(x681,x682)+~E(f11(x681,x682),a1) % 0.56/0.69 [71]~P5(x711,x712)+E(f15(x711,x712),x712) % 0.56/0.69 [76]P1(x761)+~P1(f15(x762,x761)) % 0.56/0.69 [77]P1(x771)+~P1(f15(x771,x772)) % 0.56/0.69 [78]P5(x781,x782)+P4(f7(x781,x782),x781) % 0.56/0.69 [79]P2(x791,x792)+P4(f13(x791,x792),x792) % 0.56/0.69 [80]P2(x801,x802)+P4(f13(x801,x802),x801) % 0.56/0.69 [94]P5(x941,x942)+~P4(f7(x941,x942),x942) % 0.56/0.69 [86]~P2(x861,x862)+E(f11(x861,f11(x861,x862)),a1) % 0.56/0.69 [87]~P5(x871,x872)+E(f15(x871,f11(x872,x871)),x872) % 0.56/0.69 [88]~P5(x881,x882)+E(f11(x881,f11(x881,x882)),x881) % 0.56/0.69 [93]P2(x931,x932)+~E(f11(x931,f11(x931,x932)),a1) % 0.56/0.69 [102]P2(x1021,x1022)+P4(f5(x1021,x1022),f11(x1021,f11(x1021,x1022))) % 0.56/0.69 [97]~P5(x971,x973)+P5(f11(x971,x972),f11(x973,x972)) % 0.56/0.69 [104]~P2(x1041,x1042)+~P4(x1043,f11(x1041,f11(x1041,x1042))) % 0.56/0.69 [105]~P5(x1051,x1053)+P5(f11(x1051,f11(x1051,x1052)),f11(x1053,f11(x1053,x1052))) % 0.56/0.69 [57]~P1(x572)+~P1(x571)+E(x571,x572) % 0.56/0.69 [72]P3(x721,x722)+~P5(x721,x722)+E(x721,x722) % 0.56/0.69 [75]~P5(x752,x751)+~P5(x751,x752)+E(x751,x752) % 0.56/0.69 [95]E(x951,x952)+P4(f14(x951,x952),x952)+P4(f14(x951,x952),x951) % 0.56/0.69 [101]E(x1011,x1012)+~P4(f14(x1011,x1012),x1012)+~P4(f14(x1011,x1012),x1011) % 0.56/0.69 [81]~P5(x813,x812)+P4(x811,x812)+~P4(x811,x813) % 0.56/0.69 [82]~P5(x821,x823)+P5(x821,x822)+~P5(x823,x822) % 0.56/0.69 [89]~P2(x893,x892)+~P4(x891,x892)+~P4(x891,x893) % 0.56/0.69 [96]~P5(x962,x963)+~P5(x961,x963)+P5(f15(x961,x962),x963) % 0.56/0.69 [106]P4(f9(x1062,x1063,x1061),x1061)+P4(f9(x1062,x1063,x1061),x1062)+E(x1061,f11(x1062,x1063)) % 0.56/0.69 [109]P4(f9(x1092,x1093,x1091),x1091)+~P4(f9(x1092,x1093,x1091),x1093)+E(x1091,f11(x1092,x1093)) % 0.56/0.69 [111]~P4(f8(x1112,x1113,x1111),x1111)+~P4(f8(x1112,x1113,x1111),x1113)+E(x1111,f15(x1112,x1113)) % 0.56/0.69 [112]~P4(f8(x1122,x1123,x1121),x1121)+~P4(f8(x1122,x1123,x1121),x1122)+E(x1121,f15(x1122,x1123)) % 0.56/0.69 [103]~P5(x1031,x1033)+~P5(x1031,x1032)+P5(x1031,f11(x1032,f11(x1032,x1033))) % 0.56/0.69 [107]P4(f10(x1072,x1073,x1071),x1071)+P4(f10(x1072,x1073,x1071),x1073)+E(x1071,f11(x1072,f11(x1072,x1073))) % 0.56/0.69 [108]P4(f10(x1082,x1083,x1081),x1081)+P4(f10(x1082,x1083,x1081),x1082)+E(x1081,f11(x1082,f11(x1082,x1083))) % 0.56/0.69 [83]~P4(x831,x834)+P4(x831,x832)+~E(x832,f15(x833,x834)) % 0.56/0.69 [84]~P4(x841,x843)+P4(x841,x842)+~E(x842,f15(x843,x844)) % 0.56/0.69 [85]~P4(x851,x853)+P4(x851,x852)+~E(x853,f11(x852,x854)) % 0.56/0.69 [90]~P4(x904,x903)+~P4(x904,x901)+~E(x901,f11(x902,x903)) % 0.56/0.69 [98]~P4(x981,x983)+P4(x981,x982)+~E(x983,f11(x984,f11(x984,x982))) % 0.56/0.69 [110]P4(f8(x1102,x1103,x1101),x1101)+P4(f8(x1102,x1103,x1101),x1103)+P4(f8(x1102,x1103,x1101),x1102)+E(x1101,f15(x1102,x1103)) % 0.56/0.69 [113]P4(f9(x1132,x1133,x1131),x1133)+~P4(f9(x1132,x1133,x1131),x1131)+~P4(f9(x1132,x1133,x1131),x1132)+E(x1131,f11(x1132,x1133)) % 0.56/0.69 [114]~P4(f10(x1142,x1143,x1141),x1141)+~P4(f10(x1142,x1143,x1141),x1143)+~P4(f10(x1142,x1143,x1141),x1142)+E(x1141,f11(x1142,f11(x1142,x1143))) % 0.56/0.69 [91]~P4(x911,x914)+P4(x911,x912)+P4(x911,x913)+~E(x912,f11(x914,x913)) % 0.56/0.69 [92]~P4(x921,x924)+P4(x921,x922)+P4(x921,x923)+~E(x924,f15(x923,x922)) % 0.56/0.69 [100]~P4(x1001,x1004)+~P4(x1001,x1003)+P4(x1001,x1002)+~E(x1002,f11(x1003,f11(x1003,x1004))) % 0.56/0.69 %EqnAxiom % 0.56/0.69 [1]E(x11,x11) % 0.56/0.69 [2]E(x22,x21)+~E(x21,x22) % 0.56/0.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.56/0.69 [4]~E(x41,x42)+E(f11(x41,x43),f11(x42,x43)) % 0.56/0.69 [5]~E(x51,x52)+E(f11(x53,x51),f11(x53,x52)) % 0.56/0.69 [6]~E(x61,x62)+E(f15(x61,x63),f15(x62,x63)) % 0.56/0.69 [7]~E(x71,x72)+E(f15(x73,x71),f15(x73,x72)) % 0.56/0.69 [8]~E(x81,x82)+E(f10(x81,x83,x84),f10(x82,x83,x84)) % 0.56/0.69 [9]~E(x91,x92)+E(f10(x93,x91,x94),f10(x93,x92,x94)) % 0.56/0.69 [10]~E(x101,x102)+E(f10(x103,x104,x101),f10(x103,x104,x102)) % 0.56/0.69 [11]~E(x111,x112)+E(f14(x111,x113),f14(x112,x113)) % 0.56/0.69 [12]~E(x121,x122)+E(f14(x123,x121),f14(x123,x122)) % 0.56/0.69 [13]~E(x131,x132)+E(f7(x131,x133),f7(x132,x133)) % 0.56/0.69 [14]~E(x141,x142)+E(f7(x143,x141),f7(x143,x142)) % 0.56/0.69 [15]~E(x151,x152)+E(f9(x151,x153,x154),f9(x152,x153,x154)) % 0.56/0.69 [16]~E(x161,x162)+E(f9(x163,x161,x164),f9(x163,x162,x164)) % 0.56/0.69 [17]~E(x171,x172)+E(f9(x173,x174,x171),f9(x173,x174,x172)) % 0.56/0.69 [18]~E(x181,x182)+E(f8(x181,x183,x184),f8(x182,x183,x184)) % 0.56/0.69 [19]~E(x191,x192)+E(f8(x193,x191,x194),f8(x193,x192,x194)) % 0.56/0.69 [20]~E(x201,x202)+E(f8(x203,x204,x201),f8(x203,x204,x202)) % 0.56/0.69 [21]~E(x211,x212)+E(f13(x211,x213),f13(x212,x213)) % 0.56/0.69 [22]~E(x221,x222)+E(f13(x223,x221),f13(x223,x222)) % 0.56/0.69 [23]~E(x231,x232)+E(f5(x231,x233),f5(x232,x233)) % 0.56/0.69 [24]~E(x241,x242)+E(f5(x243,x241),f5(x243,x242)) % 0.56/0.69 [25]~E(x251,x252)+E(f6(x251),f6(x252)) % 0.56/0.69 [26]~P1(x261)+P1(x262)+~E(x261,x262) % 0.56/0.69 [27]P4(x272,x273)+~E(x271,x272)+~P4(x271,x273) % 0.56/0.69 [28]P4(x283,x282)+~E(x281,x282)+~P4(x283,x281) % 0.56/0.69 [29]P3(x292,x293)+~E(x291,x292)+~P3(x291,x293) % 0.56/0.69 [30]P3(x303,x302)+~E(x301,x302)+~P3(x303,x301) % 0.56/0.69 [31]P5(x312,x313)+~E(x311,x312)+~P5(x311,x313) % 0.56/0.69 [32]P5(x323,x322)+~E(x321,x322)+~P5(x323,x321) % 0.56/0.69 [33]P2(x332,x333)+~E(x331,x332)+~P2(x331,x333) % 0.56/0.69 [34]P2(x343,x342)+~E(x341,x342)+~P2(x343,x341) % 0.56/0.69 % 0.56/0.69 %------------------------------------------- % 0.56/0.69 cnf(116,plain, % 0.56/0.69 (~P4(x1161,a1)), % 0.56/0.69 inference(equality_inference,[],[62])). % 0.56/0.69 cnf(120,plain, % 0.56/0.69 (~P4(x1201,f11(x1202,x1203))+P4(x1201,x1202)), % 0.56/0.69 inference(equality_inference,[],[85])). % 0.56/0.69 cnf(124,plain, % 0.56/0.69 (~P4(x1241,f11(x1242,f11(x1242,x1243)))+P4(x1241,x1243)), % 0.56/0.69 inference(equality_inference,[],[98])). % 0.56/0.69 cnf(137,plain, % 0.56/0.69 (E(f11(a1,x1371),a1)), % 0.56/0.69 inference(rename_variables,[],[39])). % 0.56/0.69 cnf(143,plain, % 0.56/0.69 (~P4(x1431,a1)), % 0.56/0.69 inference(rename_variables,[],[116])). % 0.56/0.69 cnf(160,plain, % 0.56/0.69 (~P3(x1601,x1601)), % 0.56/0.69 inference(rename_variables,[],[55])). % 0.56/0.69 cnf(161,plain, % 0.56/0.69 ($false), % 0.56/0.69 inference(scs_inference,[],[37,38,39,137,55,160,116,143,47,48,46,36,63,74,62,68,78,93,2,64,79,80,120,124,72,75,82,29,30]), % 0.56/0.69 ['proof']). % 0.56/0.69 % SZS output end Proof % 0.56/0.69 % Total time :0.000000s %------------------------------------------------------------------------------