%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET658+3 : TPTP v8.2.0. Released v2.2.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 14:22:09 EDT 2024 % Result : Theorem 0.55s 0.79s % Output : CNFRefutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.14 % Problem : SET658+3 : TPTP v8.2.0. Released v2.2.0. % 0.13/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n028.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Sun Jun 23 11:58:23 EDT 2024 % 0.13/0.35 % CPUTime : % 0.55/0.58 start to proof:theBenchmark % 0.55/0.77 %------------------------------------------- % 0.55/0.77 % File :CSE---1.7 % 0.55/0.77 % Problem :theBenchmark % 0.55/0.77 % Transform :cnf % 0.55/0.77 % Format :tptp:raw % 0.55/0.77 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.77 % 0.55/0.77 % Result :Theorem 0.010000s % 0.55/0.77 % Output :CNFRefutation 0.010000s % 0.55/0.77 %------------------------------------------- % 0.55/0.78 %-------------------------------------------------------------------------- % 0.55/0.78 % File : SET658+3 : TPTP v8.2.0. Released v2.2.0. % 0.55/0.79 % Domain : Set Theory (Relations) % 0.55/0.79 % Problem : Every R (X to Y) is (domain of R to range of R) % 0.55/0.79 % Version : [Wor90] axioms : Reduced > Incomplete. % 0.55/0.79 % English : Every relation R from X to Y is a relation from the domain of R % 0.55/0.79 % to the range of R. % 0.55/0.79 % 0.55/0.79 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 0.55/0.79 % : [Wor90] Woronowicz (1990), Relations Defined on Sets % 0.55/0.79 % Source : [ILF] % 0.55/0.79 % Names : RELSET_1 (20) [Wor90] % 0.55/0.79 % 0.55/0.79 % Status : Theorem % 0.55/0.79 % Rating : 0.06 v8.1.0, 0.03 v7.1.0, 0.00 v6.4.0, 0.04 v6.3.0, 0.00 v6.1.0, 0.03 v6.0.0, 0.00 v5.4.0, 0.04 v5.3.0, 0.11 v5.2.0, 0.00 v5.0.0, 0.04 v4.1.0, 0.09 v4.0.0, 0.08 v3.7.0, 0.05 v3.4.0, 0.00 v3.2.0, 0.09 v3.1.0, 0.00 v2.2.1 % 0.55/0.79 % Syntax : Number of formulae : 29 ( 2 unt; 0 def) % 0.55/0.79 % Number of atoms : 106 ( 3 equ) % 0.55/0.79 % Maximal formula atoms : 7 ( 3 avg) % 0.55/0.79 % Number of connectives : 81 ( 4 ~; 0 |; 10 &) % 0.55/0.79 % ( 9 <=>; 58 =>; 0 <=; 0 <~>) % 0.55/0.79 % Maximal formula depth : 11 ( 6 avg) % 0.55/0.79 % Maximal term depth : 3 ( 1 avg) % 0.55/0.79 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 0.55/0.79 % Number of functors : 12 ( 12 usr; 2 con; 0-3 aty) % 0.55/0.79 % Number of variables : 63 ( 55 !; 8 ?) % 0.55/0.79 % SPC : FOF_THM_RFO_SEQ % 0.55/0.79 % 0.55/0.79 % Comments : % 0.55/0.79 %-------------------------------------------------------------------------- % 0.55/0.79 %---- line(relset_1 - th(9),1916152) % 0.55/0.79 fof(p1,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,binary_relation_type) % 0.55/0.79 => ( subset(domain_of(C),B) % 0.55/0.79 => ilf_type(C,relation_type(B,range_of(C))) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- line(relat_1 - df(4),1917872) % 0.55/0.79 fof(p2,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,binary_relation_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ( member(C,domain_of(B)) % 0.55/0.79 <=> ? [D] : % 0.55/0.79 ( ilf_type(D,set_type) % 0.55/0.79 & member(ordered_pair(C,D),B) ) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- declaration(line(relat_1 - df(4),1917872)) % 0.55/0.79 fof(p3,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,binary_relation_type) % 0.55/0.79 => ilf_type(domain_of(B),set_type) ) ). % 0.55/0.79 % 0.55/0.79 %---- line(relat_1 - df(5),1917958) % 0.55/0.79 fof(p4,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,binary_relation_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ( member(C,range_of(B)) % 0.55/0.79 <=> ? [D] : % 0.55/0.79 ( ilf_type(D,set_type) % 0.55/0.79 & member(ordered_pair(D,C),B) ) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- declaration(line(relat_1 - df(5),1917958)) % 0.55/0.79 fof(p5,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,binary_relation_type) % 0.55/0.79 => ilf_type(range_of(B),set_type) ) ). % 0.55/0.79 % 0.55/0.79 %---- line(relat_1 - axiom167,1917641) % 0.55/0.79 fof(p6,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ( ilf_type(B,binary_relation_type) % 0.55/0.79 <=> ( relation_like(B) % 0.55/0.79 & ilf_type(B,set_type) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- type_nonempty(line(relat_1 - axiom167,1917641)) % 0.55/0.79 fof(p7,axiom, % 0.55/0.79 ? [B] : ilf_type(B,binary_relation_type) ). % 0.55/0.79 % 0.55/0.79 %---- line(relset_1 - df(1),1916080) % 0.55/0.79 fof(p8,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ( ! [D] : % 0.55/0.79 ( ilf_type(D,subset_type(cross_product(B,C))) % 0.55/0.79 => ilf_type(D,relation_type(B,C)) ) % 0.55/0.79 & ! [E] : % 0.55/0.79 ( ilf_type(E,relation_type(B,C)) % 0.55/0.79 => ilf_type(E,subset_type(cross_product(B,C))) ) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- type_nonempty(line(relset_1 - df(1),1916080)) % 0.55/0.79 fof(p9,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ? [D] : ilf_type(D,relation_type(C,B)) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- declaration(op(cross_product,2,function)) % 0.55/0.79 fof(p10,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ilf_type(cross_product(B,C),set_type) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- declaration(op(ordered_pair,2,function)) % 0.55/0.79 fof(p11,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ilf_type(ordered_pair(B,C),set_type) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- line(hidden - axiom168,1832648) % 0.55/0.79 fof(p12,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ( ilf_type(C,subset_type(B)) % 0.55/0.79 <=> ilf_type(C,member_type(power_set(B))) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- type_nonempty(line(hidden - axiom168,1832648)) % 0.55/0.79 fof(p13,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ? [C] : ilf_type(C,subset_type(B)) ) ). % 0.55/0.79 % 0.55/0.79 %---- line(tarski - df(3),1832749) % 0.55/0.79 fof(p14,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ( subset(B,C) % 0.55/0.79 <=> ! [D] : % 0.55/0.79 ( ilf_type(D,set_type) % 0.55/0.79 => ( member(D,B) % 0.55/0.79 => member(D,C) ) ) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- property(reflexivity,op(subset,2,predicate)) % 0.55/0.79 fof(p15,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => subset(B,B) ) ). % 0.55/0.79 % 0.55/0.79 %---- line(relat_1 - df(1),1917627) % 0.55/0.79 fof(p16,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ( relation_like(B) % 0.55/0.79 <=> ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ( member(C,B) % 0.55/0.79 => ? [D] : % 0.55/0.79 ( ilf_type(D,set_type) % 0.55/0.79 & ? [E] : % 0.55/0.79 ( ilf_type(E,set_type) % 0.55/0.79 & C = ordered_pair(D,E) ) ) ) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- conditional_cluster(axiom171,relation_like) % 0.55/0.79 fof(p17,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ! [D] : % 0.55/0.79 ( ilf_type(D,subset_type(cross_product(B,C))) % 0.55/0.79 => relation_like(D) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- line(hidden - axiom172,1832644) % 0.55/0.79 fof(p18,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ( member(B,power_set(C)) % 0.55/0.79 <=> ! [D] : % 0.55/0.79 ( ilf_type(D,set_type) % 0.55/0.79 => ( member(D,B) % 0.55/0.79 => member(D,C) ) ) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- declaration(line(hidden - axiom172,1832644)) % 0.55/0.79 fof(p19,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ( ~ empty(power_set(B)) % 0.55/0.79 & ilf_type(power_set(B),set_type) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- line(hidden - axiom173,1832640) % 0.55/0.79 fof(p20,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ( ~ empty(C) % 0.55/0.79 & ilf_type(C,set_type) ) % 0.55/0.79 => ( ilf_type(B,member_type(C)) % 0.55/0.79 <=> member(B,C) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- type_nonempty(line(hidden - axiom173,1832640)) % 0.55/0.79 fof(p21,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ( ~ empty(B) % 0.55/0.79 & ilf_type(B,set_type) ) % 0.55/0.79 => ? [C] : ilf_type(C,member_type(B)) ) ). % 0.55/0.79 % 0.55/0.79 %---- line(hidden - axiom174,1832628) % 0.55/0.79 fof(p22,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ( empty(B) % 0.55/0.79 <=> ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ~ member(C,B) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- conditional_cluster(axiom175,empty) % 0.55/0.79 fof(p23,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ( empty(B) % 0.55/0.79 & ilf_type(B,set_type) ) % 0.55/0.79 => relation_like(B) ) ). % 0.55/0.79 % 0.55/0.79 %---- line(relset_1 - axiom179,1916330) % 0.55/0.79 fof(p24,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ! [D] : % 0.55/0.79 ( ilf_type(D,relation_type(B,C)) % 0.55/0.79 => domain(B,C,D) = domain_of(D) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- declaration(line(relset_1 - axiom179,1916330)) % 0.55/0.79 fof(p25,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ! [D] : % 0.55/0.79 ( ilf_type(D,relation_type(B,C)) % 0.55/0.79 => ilf_type(domain(B,C,D),subset_type(B)) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- line(relset_1 - axiom180,1916334) % 0.55/0.79 fof(p26,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ! [D] : % 0.55/0.79 ( ilf_type(D,relation_type(B,C)) % 0.55/0.79 => range(B,C,D) = range_of(D) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- declaration(line(relset_1 - axiom180,1916334)) % 0.55/0.79 fof(p27,axiom, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,set_type) % 0.55/0.79 => ! [C] : % 0.55/0.79 ( ilf_type(C,set_type) % 0.55/0.79 => ! [D] : % 0.55/0.79 ( ilf_type(D,relation_type(B,C)) % 0.55/0.79 => ilf_type(range(B,C,D),subset_type(C)) ) ) ) ). % 0.55/0.79 % 0.55/0.79 %---- declaration(set) % 0.55/0.79 fof(p28,axiom, % 0.55/0.79 ! [B] : ilf_type(B,set_type) ). % 0.55/0.79 % 0.55/0.79 %---- line(relset_1 - th(20),1916347) % 0.55/0.79 fof(prove_relset_1_20,conjecture, % 0.55/0.79 ! [B] : % 0.55/0.79 ( ilf_type(B,binary_relation_type) % 0.55/0.79 => ilf_type(B,relation_type(domain_of(B),range_of(B))) ) ). % 0.55/0.79 % 0.55/0.79 %-------------------------------------------------------------------------- % 0.55/0.79 %------------------------------------------- % 0.55/0.79 % Proof found % 0.55/0.79 % SZS status Theorem for theBenchmark % 0.55/0.79 % SZS output start Proof % 0.55/0.79 %ClaNum:98(EqnAxiom:46) % 0.55/0.79 %VarNum:227(SingletonVarNum:74) % 0.55/0.79 %MaxLitNum:6 % 0.55/0.79 %MaxfuncDepth:2 % 0.55/0.79 %SharedTerms:10 % 0.55/0.79 %goalClause: 48 50 % 0.55/0.79 %singleGoalClaCount:2 % 0.55/0.80 [47]P1(a1,a2) % 0.55/0.80 [48]P1(a3,a2) % 0.55/0.80 [50]~P1(a3,f24(f4(a3),f13(a3))) % 0.55/0.80 [49]P1(x491,a12) % 0.55/0.80 [52]P5(x521,x521)+~P1(x521,a12) % 0.55/0.80 [53]~P1(x531,a12)+~P2(f14(x531)) % 0.55/0.80 [63]~P1(x631,a12)+P1(f16(x631),f25(x631)) % 0.55/0.80 [51]~P2(x511)+P3(x511)+~P1(x511,a12) % 0.55/0.80 [57]~P3(x571)+~P1(x571,a12)+P1(x571,a2) % 0.55/0.80 [60]P3(x601)+~P1(x601,a12)+~P1(x601,a2) % 0.55/0.80 [61]P3(x611)+P4(f15(x611),x611)+~P1(x611,a12) % 0.55/0.80 [62]P2(x621)+P4(f7(x621),x621)+~P1(x621,a12) % 0.55/0.80 [64]P2(x641)+P1(f8(x641),f21(x641))+~P1(x641,a12) % 0.55/0.80 [76]~P1(x762,a12)+~P1(x761,a12)+P1(f17(x761,x762),f24(x762,x761)) % 0.55/0.80 [65]~P2(x651)+~P4(x652,x651)+~P1(x652,a12)+~P1(x651,a12) % 0.55/0.80 [72]P5(x721,x722)+P4(f18(x721,x722),x721)+~P1(x722,a12)+~P1(x721,a12) % 0.55/0.80 [74]P4(f9(x741,x742),x741)+~P1(x742,a12)+~P1(x741,a12)+P4(x741,f14(x742)) % 0.55/0.80 [82]P5(x821,x822)+~P1(x822,a12)+~P1(x821,a12)+~P4(f18(x821,x822),x822) % 0.55/0.80 [84]~P1(x842,a12)+~P1(x841,a12)+~P4(f9(x841,x842),x842)+P4(x841,f14(x842)) % 0.55/0.80 [75]~P1(x752,a12)+~P1(x751,a12)+~P1(x751,f25(x752))+P1(x751,f21(f14(x752))) % 0.55/0.80 [81]~P1(x812,a12)+~P1(x811,a12)+P1(x811,f25(x812))+~P1(x811,f21(f14(x812))) % 0.55/0.80 [85]~P1(x851,a2)+~P1(x852,a12)+~P5(f4(x851),x852)+P1(x851,f24(x852,f13(x851))) % 0.55/0.80 [93]~P1(x932,a2)+~P1(x931,a12)+~P4(x931,f4(x932))+P4(f22(x931,f10(x932,x931)),x932) % 0.55/0.80 [94]~P1(x942,a12)+~P1(x941,a2)+~P4(x942,f13(x941))+P4(f22(f11(x941,x942),x942),x941) % 0.55/0.80 [91]~P1(x912,a12)+~P1(x911,a12)+~P1(x913,f24(x911,x912))+E(f6(x911,x912,x913),f4(x913)) % 0.55/0.80 [92]~P1(x922,a12)+~P1(x921,a12)+~P1(x923,f24(x921,x922))+E(f23(x921,x922,x923),f13(x923)) % 0.55/0.80 [97]~P1(x972,a12)+~P1(x971,a12)+~P1(x973,f24(x971,x972))+P1(f6(x971,x972,x973),f25(x971)) % 0.55/0.80 [98]~P1(x982,a12)+~P1(x981,a12)+~P1(x983,f24(x981,x982))+P1(f23(x981,x982,x983),f25(x982)) % 0.55/0.80 [90]P3(x901)+~P1(x902,a12)+~P1(x903,a12)+~P1(x901,f25(f5(x903,x902))) % 0.55/0.80 [95]~P1(x953,a12)+~P1(x952,a12)+~P1(x951,f24(x952,x953))+P1(x951,f25(f5(x952,x953))) % 0.55/0.80 [96]~P1(x963,a12)+~P1(x962,a12)+P1(x961,f24(x962,x963))+~P1(x961,f25(f5(x962,x963))) % 0.55/0.80 [68]~P4(x682,x681)+P2(x681)+~P1(x681,a12)+~P1(x682,a12)+P1(x682,f21(x681)) % 0.55/0.80 [69]P2(x691)+P4(x692,x691)+~P1(x691,a12)+~P1(x692,a12)+~P1(x692,f21(x691)) % 0.55/0.80 [87]~P3(x871)+~P4(x872,x871)+~P1(x871,a12)+~P1(x872,a12)+E(f22(f19(x871,x872),f20(x871,x872)),x872) % 0.55/0.80 [71]P3(x711)+~P1(x711,a12)+~P1(x713,a12)+~P1(x712,a12)+~E(f15(x711),f22(x712,x713)) % 0.55/0.80 [88]~P1(x882,a2)+~P1(x881,a12)+~P4(f22(x881,x883),x882)+P4(x881,f4(x882))+~P1(x883,a12) % 0.55/0.80 [89]~P1(x892,a2)+~P1(x891,a12)+~P4(f22(x893,x891),x892)+P4(x891,f13(x892))+~P1(x893,a12) % 0.55/0.80 [83]~P4(x831,x833)+P4(x831,x832)+~P5(x833,x832)+~P1(x831,a12)+~P1(x832,a12)+~P1(x833,a12) % 0.55/0.80 [86]P4(x861,x862)+~P4(x861,x863)+~P1(x861,a12)+~P1(x862,a12)+~P1(x863,a12)+~P4(x863,f14(x862)) % 0.55/0.80 %EqnAxiom % 0.55/0.80 [1]E(x11,x11) % 0.55/0.80 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.80 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.80 [4]~E(x41,x42)+E(f4(x41),f4(x42)) % 0.55/0.80 [5]~E(x51,x52)+E(f13(x51),f13(x52)) % 0.55/0.80 [6]~E(x61,x62)+E(f24(x61,x63),f24(x62,x63)) % 0.55/0.80 [7]~E(x71,x72)+E(f24(x73,x71),f24(x73,x72)) % 0.55/0.80 [8]~E(x81,x82)+E(f14(x81),f14(x82)) % 0.55/0.80 [9]~E(x91,x92)+E(f5(x91,x93),f5(x92,x93)) % 0.55/0.80 [10]~E(x101,x102)+E(f5(x103,x101),f5(x103,x102)) % 0.55/0.80 [11]~E(x111,x112)+E(f25(x111),f25(x112)) % 0.55/0.80 [12]~E(x121,x122)+E(f23(x121,x123,x124),f23(x122,x123,x124)) % 0.55/0.80 [13]~E(x131,x132)+E(f23(x133,x131,x134),f23(x133,x132,x134)) % 0.55/0.80 [14]~E(x141,x142)+E(f23(x143,x144,x141),f23(x143,x144,x142)) % 0.55/0.80 [15]~E(x151,x152)+E(f15(x151),f15(x152)) % 0.55/0.80 [16]~E(x161,x162)+E(f7(x161),f7(x162)) % 0.55/0.80 [17]~E(x171,x172)+E(f22(x171,x173),f22(x172,x173)) % 0.55/0.80 [18]~E(x181,x182)+E(f22(x183,x181),f22(x183,x182)) % 0.55/0.80 [19]~E(x191,x192)+E(f21(x191),f21(x192)) % 0.55/0.80 [20]~E(x201,x202)+E(f16(x201),f16(x202)) % 0.55/0.80 [21]~E(x211,x212)+E(f11(x211,x213),f11(x212,x213)) % 0.55/0.80 [22]~E(x221,x222)+E(f11(x223,x221),f11(x223,x222)) % 0.55/0.80 [23]~E(x231,x232)+E(f8(x231),f8(x232)) % 0.55/0.80 [24]~E(x241,x242)+E(f20(x241,x243),f20(x242,x243)) % 0.55/0.80 [25]~E(x251,x252)+E(f20(x253,x251),f20(x253,x252)) % 0.55/0.80 [26]~E(x261,x262)+E(f6(x261,x263,x264),f6(x262,x263,x264)) % 0.55/0.80 [27]~E(x271,x272)+E(f6(x273,x271,x274),f6(x273,x272,x274)) % 0.55/0.80 [28]~E(x281,x282)+E(f6(x283,x284,x281),f6(x283,x284,x282)) % 0.55/0.80 [29]~E(x291,x292)+E(f10(x291,x293),f10(x292,x293)) % 0.55/0.80 [30]~E(x301,x302)+E(f10(x303,x301),f10(x303,x302)) % 0.55/0.80 [31]~E(x311,x312)+E(f19(x311,x313),f19(x312,x313)) % 0.55/0.80 [32]~E(x321,x322)+E(f19(x323,x321),f19(x323,x322)) % 0.55/0.80 [33]~E(x331,x332)+E(f9(x331,x333),f9(x332,x333)) % 0.55/0.80 [34]~E(x341,x342)+E(f9(x343,x341),f9(x343,x342)) % 0.55/0.80 [35]~E(x351,x352)+E(f18(x351,x353),f18(x352,x353)) % 0.55/0.80 [36]~E(x361,x362)+E(f18(x363,x361),f18(x363,x362)) % 0.55/0.80 [37]~E(x371,x372)+E(f17(x371,x373),f17(x372,x373)) % 0.55/0.80 [38]~E(x381,x382)+E(f17(x383,x381),f17(x383,x382)) % 0.55/0.80 [39]P1(x392,x393)+~E(x391,x392)+~P1(x391,x393) % 0.55/0.80 [40]P1(x403,x402)+~E(x401,x402)+~P1(x403,x401) % 0.55/0.80 [41]P4(x412,x413)+~E(x411,x412)+~P4(x411,x413) % 0.55/0.80 [42]P4(x423,x422)+~E(x421,x422)+~P4(x423,x421) % 0.55/0.80 [43]~P2(x431)+P2(x432)+~E(x431,x432) % 0.55/0.80 [44]P5(x442,x443)+~E(x441,x442)+~P5(x441,x443) % 0.55/0.80 [45]P5(x453,x452)+~E(x451,x452)+~P5(x453,x451) % 0.55/0.80 [46]~P3(x461)+P3(x462)+~E(x461,x462) % 0.55/0.80 % 0.55/0.80 %------------------------------------------- % 0.55/0.80 cnf(99,plain, % 0.55/0.80 (P5(x991,x991)), % 0.55/0.80 inference(scs_inference,[],[49,52])). % 0.55/0.80 cnf(102,plain, % 0.55/0.80 (P1(x1021,a12)), % 0.55/0.80 inference(rename_variables,[],[49])). % 0.55/0.80 cnf(105,plain, % 0.55/0.80 (~P5(f4(a3),f4(a3))), % 0.55/0.80 inference(scs_inference,[],[48,50,49,102,52,60,40,85])). % 0.55/0.80 cnf(126,plain, % 0.55/0.80 ($false), % 0.55/0.80 inference(scs_inference,[],[105,99]), % 0.55/0.80 ['proof']). % 0.55/0.80 % SZS output end Proof % 0.55/0.80 % Total time :0.010000s %------------------------------------------------------------------------------