%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET682+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 : n026.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:13 EDT 2024 % Result : Theorem 65.13s 65.17s % Output : CNFRefutation 65.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET682+3 : TPTP v8.2.0. Released v2.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 17:53:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.21/0.57 start to proof:theBenchmark % 65.13/65.15 %------------------------------------------- % 65.13/65.15 % File :CSE---1.7 % 65.13/65.15 % Problem :theBenchmark % 65.13/65.15 % Transform :cnf % 65.13/65.15 % Format :tptp:raw % 65.13/65.15 % Command :java -jar mcs_scs.jar %d %s % 65.13/65.15 % 65.13/65.15 % Result :Theorem 64.530000s % 65.13/65.15 % Output :CNFRefutation 64.530000s % 65.13/65.15 %------------------------------------------- % 65.13/65.17 %-------------------------------------------------------------------------- % 65.13/65.17 % File : SET682+3 : TPTP v8.2.0. Released v2.2.0. % 65.13/65.17 % Domain : Set Theory (Relations) % 65.13/65.17 % Problem : !x in D : x in domain of R (X to Y) ? y in E : y in range of R % 65.13/65.17 % Version : [Wor90] axioms : Reduced > Incomplete. % 65.13/65.17 % English : For every element x in D such that x is in the domain of a % 65.13/65.17 % relation R from X to Y there exists an element y in E such that % 65.13/65.17 % y is in the range of R. % 65.13/65.17 % 65.13/65.17 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 65.13/65.17 % : [Wor90] Woronowicz (1990), Relations Defined on Sets % 65.13/65.17 % Source : [ILF] % 65.13/65.17 % Names : RELSET_1 (49) [Wor90] % 65.13/65.17 % 65.13/65.17 % Status : Theorem % 65.13/65.17 % Rating : 0.36 v8.2.0, 0.39 v8.1.0, 0.44 v7.4.0, 0.37 v7.3.0, 0.45 v7.2.0, 0.41 v7.1.0, 0.35 v7.0.0, 0.30 v6.4.0, 0.35 v6.3.0, 0.38 v6.2.0, 0.40 v6.1.0, 0.37 v6.0.0, 0.35 v5.5.0, 0.30 v5.4.0, 0.32 v5.3.0, 0.37 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.33 v4.1.0, 0.35 v4.0.0, 0.33 v3.7.0, 0.30 v3.5.0, 0.26 v3.3.0, 0.21 v3.2.0, 0.18 v3.1.0, 0.22 v2.7.0, 0.50 v2.6.0, 0.29 v2.5.0, 0.25 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1 % 65.13/65.17 % Syntax : Number of formulae : 25 ( 2 unt; 0 def) % 65.13/65.17 % Number of atoms : 96 ( 3 equ) % 65.13/65.17 % Maximal formula atoms : 9 ( 3 avg) % 65.13/65.17 % Number of connectives : 77 ( 6 ~; 0 |; 12 &) % 65.13/65.17 % ( 6 <=>; 53 =>; 0 <=; 0 <~>) % 65.13/65.17 % Maximal formula depth : 12 ( 6 avg) % 65.13/65.17 % Maximal term depth : 3 ( 1 avg) % 65.13/65.17 % Number of predicates : 5 ( 4 usr; 0 prp; 1-2 aty) % 65.13/65.17 % Number of functors : 12 ( 12 usr; 2 con; 0-3 aty) % 65.13/65.17 % Number of variables : 58 ( 50 !; 8 ?) % 65.13/65.17 % SPC : FOF_THM_RFO_SEQ % 65.13/65.17 % 65.13/65.17 % Comments : % 65.13/65.17 %-------------------------------------------------------------------------- % 65.13/65.17 %---- line(relat_1 - th(18),1917973) % 65.13/65.17 fof(p1,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,binary_relation_type) % 65.13/65.17 => ( member(B,domain_of(C)) % 65.13/65.17 => ? [D] : % 65.13/65.17 ( ilf_type(D,set_type) % 65.13/65.17 & member(D,range_of(C)) ) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- line(relset_1 - df(1),1916080) % 65.13/65.17 fof(p2,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ( ! [D] : % 65.13/65.17 ( ilf_type(D,subset_type(cross_product(B,C))) % 65.13/65.17 => ilf_type(D,relation_type(B,C)) ) % 65.13/65.17 & ! [E] : % 65.13/65.17 ( ilf_type(E,relation_type(B,C)) % 65.13/65.17 => ilf_type(E,subset_type(cross_product(B,C))) ) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- type_nonempty(line(relset_1 - df(1),1916080)) % 65.13/65.17 fof(p3,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ? [D] : ilf_type(D,relation_type(C,B)) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- line(hidden - axiom628,1832640) % 65.13/65.17 fof(p4,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ( ~ empty(C) % 65.13/65.17 & ilf_type(C,set_type) ) % 65.13/65.17 => ( ilf_type(B,member_type(C)) % 65.13/65.17 <=> member(B,C) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- type_nonempty(line(hidden - axiom628,1832640)) % 65.13/65.17 fof(p5,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ( ~ empty(B) % 65.13/65.17 & ilf_type(B,set_type) ) % 65.13/65.17 => ? [C] : ilf_type(C,member_type(B)) ) ). % 65.13/65.17 % 65.13/65.17 %---- line(hidden - axiom630,1832628) % 65.13/65.17 fof(p6,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ( empty(B) % 65.13/65.17 <=> ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ~ member(C,B) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- declaration(op(domain_of,1,function)) % 65.13/65.17 fof(p7,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,binary_relation_type) % 65.13/65.17 => ilf_type(domain_of(B),set_type) ) ). % 65.13/65.17 % 65.13/65.17 %---- declaration(op(cross_product,2,function)) % 65.13/65.17 fof(p8,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ilf_type(cross_product(B,C),set_type) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- declaration(op(range_of,1,function)) % 65.13/65.17 fof(p9,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,binary_relation_type) % 65.13/65.17 => ilf_type(range_of(B),set_type) ) ). % 65.13/65.17 % 65.13/65.17 %---- line(relat_1 - axiom631,1917641) % 65.13/65.17 fof(p10,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ( ilf_type(B,binary_relation_type) % 65.13/65.17 <=> ( relation_like(B) % 65.13/65.17 & ilf_type(B,set_type) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- type_nonempty(line(relat_1 - axiom631,1917641)) % 65.13/65.17 fof(p11,axiom, % 65.13/65.17 ? [B] : ilf_type(B,binary_relation_type) ). % 65.13/65.17 % 65.13/65.17 %---- line(hidden - axiom632,1832648) % 65.13/65.17 fof(p12,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ( ilf_type(C,subset_type(B)) % 65.13/65.17 <=> ilf_type(C,member_type(power_set(B))) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- type_nonempty(line(hidden - axiom632,1832648)) % 65.13/65.17 fof(p13,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ? [C] : ilf_type(C,subset_type(B)) ) ). % 65.13/65.17 % 65.13/65.17 %---- line(hidden - axiom634,1832644) % 65.13/65.17 fof(p14,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ( member(B,power_set(C)) % 65.13/65.17 <=> ! [D] : % 65.13/65.17 ( ilf_type(D,set_type) % 65.13/65.17 => ( member(D,B) % 65.13/65.17 => member(D,C) ) ) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- declaration(line(hidden - axiom634,1832644)) % 65.13/65.17 fof(p15,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ( ~ empty(power_set(B)) % 65.13/65.17 & ilf_type(power_set(B),set_type) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- line(relat_1 - df(1),1917627) % 65.13/65.17 fof(p16,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ( relation_like(B) % 65.13/65.17 <=> ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ( member(C,B) % 65.13/65.17 => ? [D] : % 65.13/65.17 ( ilf_type(D,set_type) % 65.13/65.17 & ? [E] : % 65.13/65.17 ( ilf_type(E,set_type) % 65.13/65.17 & C = ordered_pair(D,E) ) ) ) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- conditional_cluster(axiom635,relation_like) % 65.13/65.17 fof(p17,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ( empty(B) % 65.13/65.17 & ilf_type(B,set_type) ) % 65.13/65.17 => relation_like(B) ) ). % 65.13/65.17 % 65.13/65.17 %---- conditional_cluster(axiom636,relation_like) % 65.13/65.17 fof(p18,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ! [D] : % 65.13/65.17 ( ilf_type(D,subset_type(cross_product(B,C))) % 65.13/65.17 => relation_like(D) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- declaration(op(ordered_pair,2,function)) % 65.13/65.17 fof(p19,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ilf_type(ordered_pair(B,C),set_type) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- line(relset_1 - axiom640,1916330) % 65.13/65.17 fof(p20,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ! [D] : % 65.13/65.17 ( ilf_type(D,relation_type(B,C)) % 65.13/65.17 => domain(B,C,D) = domain_of(D) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- declaration(line(relset_1 - axiom640,1916330)) % 65.13/65.17 fof(p21,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ! [D] : % 65.13/65.17 ( ilf_type(D,relation_type(B,C)) % 65.13/65.17 => ilf_type(domain(B,C,D),subset_type(B)) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- line(relset_1 - axiom641,1916334) % 65.13/65.17 fof(p22,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ! [D] : % 65.13/65.17 ( ilf_type(D,relation_type(B,C)) % 65.13/65.17 => range(B,C,D) = range_of(D) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- declaration(line(relset_1 - axiom641,1916334)) % 65.13/65.17 fof(p23,axiom, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ilf_type(B,set_type) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ilf_type(C,set_type) % 65.13/65.17 => ! [D] : % 65.13/65.17 ( ilf_type(D,relation_type(B,C)) % 65.13/65.17 => ilf_type(range(B,C,D),subset_type(C)) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %---- declaration(set) % 65.13/65.17 fof(p24,axiom, % 65.13/65.17 ! [B] : ilf_type(B,set_type) ). % 65.13/65.17 % 65.13/65.17 %---- line(relset_1 - th(49),1916922) % 65.13/65.17 fof(prove_relset_1_49,conjecture, % 65.13/65.17 ! [B] : % 65.13/65.17 ( ( ~ empty(B) % 65.13/65.17 & ilf_type(B,set_type) ) % 65.13/65.17 => ! [C] : % 65.13/65.17 ( ( ~ empty(C) % 65.13/65.17 & ilf_type(C,set_type) ) % 65.13/65.17 => ! [D] : % 65.13/65.17 ( ilf_type(D,relation_type(B,C)) % 65.13/65.17 => ! [E] : % 65.13/65.17 ( ilf_type(E,member_type(B)) % 65.13/65.17 => ( member(E,domain(B,C,D)) % 65.13/65.17 => ? [F] : % 65.13/65.17 ( ilf_type(F,member_type(C)) % 65.13/65.17 & member(F,range(B,C,D)) ) ) ) ) ) ) ). % 65.13/65.17 % 65.13/65.17 %-------------------------------------------------------------------------- % 65.13/65.17 %------------------------------------------- % 65.13/65.17 % Proof found % 65.13/65.17 % SZS status Theorem for theBenchmark % 65.13/65.17 % SZS output start Proof % 65.13/65.17 %ClaNum:88(EqnAxiom:40) % 65.13/65.17 %VarNum:171(SingletonVarNum:57) % 65.13/65.17 %MaxLitNum:6 % 65.13/65.17 %MaxfuncDepth:2 % 65.13/65.17 %SharedTerms:20 % 65.13/65.17 %goalClause: 45 46 47 48 49 86 % 65.13/65.17 %singleGoalClaCount:5 % 65.13/65.17 [41]P1(a1,a2) % 65.13/65.17 [48]~P2(a3) % 65.13/65.17 [49]~P2(a8) % 65.13/65.17 [45]P1(a9,f16(a3)) % 65.13/65.17 [46]P1(a10,f21(a3,a8)) % 65.13/65.17 [47]P3(a9,f4(a3,a8,a10)) % 65.13/65.17 [44]P1(x441,a15) % 65.13/65.17 [51]~P1(x511,a15)+~P2(f22(x511)) % 65.13/65.17 [61]~P1(x611,a15)+P1(f17(x611),f26(x611)) % 65.13/65.17 [86]~P3(x861,f25(a3,a8,a10))+~P1(x861,f16(a8)) % 65.13/65.17 [50]~P2(x501)+P4(x501)+~P1(x501,a15) % 65.13/65.17 [55]~P4(x551)+~P1(x551,a15)+P1(x551,a2) % 65.13/65.17 [58]P4(x581)+~P1(x581,a15)+~P1(x581,a2) % 65.13/65.17 [59]P2(x591)+P3(f11(x591),x591)+~P1(x591,a15) % 65.13/65.17 [60]P4(x601)+P3(f7(x601),x601)+~P1(x601,a15) % 65.13/65.17 [62]P2(x621)+P1(f12(x621),f16(x621))+~P1(x621,a15) % 65.13/65.17 [72]~P1(x722,a15)+~P1(x721,a15)+P1(f13(x721,x722),f21(x722,x721)) % 65.13/65.17 [63]~P2(x631)+~P3(x632,x631)+~P1(x632,a15)+~P1(x631,a15) % 65.13/65.17 [70]P3(f18(x701,x702),x701)+~P1(x702,a15)+~P1(x701,a15)+P3(x701,f22(x702)) % 65.13/65.17 [77]~P1(x772,a2)+~P1(x771,a15)+~P3(x771,f6(x772))+P3(f14(x771,x772),f24(x772)) % 65.13/65.17 [78]~P1(x782,a15)+~P1(x781,a15)+~P3(f18(x781,x782),x782)+P3(x781,f22(x782)) % 65.13/65.17 [71]~P1(x712,a15)+~P1(x711,a15)+~P1(x711,f26(x712))+P1(x711,f16(f22(x712))) % 65.13/65.17 [76]~P1(x762,a15)+~P1(x761,a15)+P1(x761,f26(x762))+~P1(x761,f16(f22(x762))) % 65.13/65.17 [82]~P1(x822,a15)+~P1(x821,a15)+~P1(x823,f21(x821,x822))+E(f4(x821,x822,x823),f6(x823)) % 65.13/65.17 [83]~P1(x832,a15)+~P1(x831,a15)+~P1(x833,f21(x831,x832))+E(f25(x831,x832,x833),f24(x833)) % 65.13/65.17 [87]~P1(x872,a15)+~P1(x871,a15)+~P1(x873,f21(x871,x872))+P1(f4(x871,x872,x873),f26(x871)) % 65.13/65.17 [88]~P1(x882,a15)+~P1(x881,a15)+~P1(x883,f21(x881,x882))+P1(f25(x881,x882,x883),f26(x882)) % 65.13/65.17 [81]P4(x811)+~P1(x812,a15)+~P1(x813,a15)+~P1(x811,f26(f5(x813,x812))) % 65.13/65.17 [84]~P1(x843,a15)+~P1(x842,a15)+~P1(x841,f21(x842,x843))+P1(x841,f26(f5(x842,x843))) % 65.13/65.17 [85]~P1(x853,a15)+~P1(x852,a15)+P1(x851,f21(x852,x853))+~P1(x851,f26(f5(x852,x853))) % 65.13/65.17 [66]~P3(x662,x661)+P2(x661)+~P1(x661,a15)+~P1(x662,a15)+P1(x662,f16(x661)) % 65.13/65.17 [67]P2(x671)+P3(x672,x671)+~P1(x671,a15)+~P1(x672,a15)+~P1(x672,f16(x671)) % 65.13/65.17 [80]~P4(x801)+~P3(x802,x801)+~P1(x801,a15)+~P1(x802,a15)+E(f23(f19(x801,x802),f20(x801,x802)),x802) % 65.13/65.17 [68]P4(x681)+~P1(x681,a15)+~P1(x683,a15)+~P1(x682,a15)+~E(f7(x681),f23(x682,x683)) % 65.13/65.17 [79]P3(x791,x792)+~P3(x791,x793)+~P1(x791,a15)+~P1(x792,a15)+~P1(x793,a15)+~P3(x793,f22(x792)) % 65.13/65.17 %EqnAxiom % 65.13/65.17 [1]E(x11,x11) % 65.13/65.17 [2]E(x22,x21)+~E(x21,x22) % 65.13/65.17 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 65.13/65.17 [4]~E(x41,x42)+E(f16(x41),f16(x42)) % 65.13/65.17 [5]~E(x51,x52)+E(f21(x51,x53),f21(x52,x53)) % 65.13/65.17 [6]~E(x61,x62)+E(f21(x63,x61),f21(x63,x62)) % 65.13/65.17 [7]~E(x71,x72)+E(f4(x71,x73,x74),f4(x72,x73,x74)) % 65.13/65.17 [8]~E(x81,x82)+E(f4(x83,x81,x84),f4(x83,x82,x84)) % 65.13/65.17 [9]~E(x91,x92)+E(f4(x93,x94,x91),f4(x93,x94,x92)) % 65.13/65.17 [10]~E(x101,x102)+E(f22(x101),f22(x102)) % 65.13/65.17 [11]~E(x111,x112)+E(f6(x111),f6(x112)) % 65.13/65.17 [12]~E(x121,x122)+E(f24(x121),f24(x122)) % 65.13/65.17 [13]~E(x131,x132)+E(f5(x131,x133),f5(x132,x133)) % 65.13/65.17 [14]~E(x141,x142)+E(f5(x143,x141),f5(x143,x142)) % 65.13/65.17 [15]~E(x151,x152)+E(f11(x151),f11(x152)) % 65.13/65.17 [16]~E(x161,x162)+E(f7(x161),f7(x162)) % 65.13/65.17 [17]~E(x171,x172)+E(f14(x171,x173),f14(x172,x173)) % 65.13/65.17 [18]~E(x181,x182)+E(f14(x183,x181),f14(x183,x182)) % 65.13/65.17 [19]~E(x191,x192)+E(f26(x191),f26(x192)) % 65.13/65.17 [20]~E(x201,x202)+E(f17(x201),f17(x202)) % 65.13/65.17 [21]~E(x211,x212)+E(f20(x211,x213),f20(x212,x213)) % 65.13/65.18 [22]~E(x221,x222)+E(f20(x223,x221),f20(x223,x222)) % 65.13/65.18 [23]~E(x231,x232)+E(f12(x231),f12(x232)) % 65.13/65.18 [24]~E(x241,x242)+E(f25(x241,x243,x244),f25(x242,x243,x244)) % 65.13/65.18 [25]~E(x251,x252)+E(f25(x253,x251,x254),f25(x253,x252,x254)) % 65.13/65.18 [26]~E(x261,x262)+E(f25(x263,x264,x261),f25(x263,x264,x262)) % 65.13/65.18 [27]~E(x271,x272)+E(f18(x271,x273),f18(x272,x273)) % 65.13/65.18 [28]~E(x281,x282)+E(f18(x283,x281),f18(x283,x282)) % 65.13/65.18 [29]~E(x291,x292)+E(f23(x291,x293),f23(x292,x293)) % 65.13/65.18 [30]~E(x301,x302)+E(f23(x303,x301),f23(x303,x302)) % 65.13/65.18 [31]~E(x311,x312)+E(f19(x311,x313),f19(x312,x313)) % 65.13/65.18 [32]~E(x321,x322)+E(f19(x323,x321),f19(x323,x322)) % 65.13/65.18 [33]~E(x331,x332)+E(f13(x331,x333),f13(x332,x333)) % 65.13/65.18 [34]~E(x341,x342)+E(f13(x343,x341),f13(x343,x342)) % 65.13/65.18 [35]P1(x352,x353)+~E(x351,x352)+~P1(x351,x353) % 65.13/65.18 [36]P1(x363,x362)+~E(x361,x362)+~P1(x363,x361) % 65.13/65.18 [37]P3(x372,x373)+~E(x371,x372)+~P3(x371,x373) % 65.13/65.18 [38]P3(x383,x382)+~E(x381,x382)+~P3(x383,x381) % 65.13/65.18 [39]~P4(x391)+P4(x392)+~E(x391,x392) % 65.13/65.18 [40]~P2(x401)+P2(x402)+~E(x401,x402) % 65.13/65.18 % 65.13/65.18 %------------------------------------------- % 65.13/65.19 cnf(102,plain, % 65.13/65.19 (P4(x1021)+~P2(x1021)), % 65.13/65.19 inference(scs_inference,[],[44,50])). % 65.13/65.19 cnf(141,plain, % 65.13/65.19 (P1(x1411,x1412)+~E(a15,x1412)), % 65.13/65.19 inference(scs_inference,[],[44,36])). % 65.13/65.19 cnf(186,plain, % 65.13/65.19 (~E(f4(a3,a8,a10),f6(a1))+P3(f14(a9,a1),f24(a1))), % 65.13/65.19 inference(scs_inference,[],[47,44,41,38,77])). % 65.13/65.19 cnf(193,plain, % 65.13/65.19 (~P2(x1931)+~P3(x1931,x1931)), % 65.13/65.19 inference(scs_inference,[],[44,63])). % 65.13/65.19 cnf(195,plain, % 65.13/65.19 (P3(x1951,f22(x1951))+P3(f18(x1951,x1951),x1951)), % 65.13/65.19 inference(scs_inference,[],[44,63,70])). % 65.13/65.19 cnf(240,plain, % 65.13/65.19 (~P3(a8,a8)+~P3(a8,f25(a3,a8,a10))), % 65.13/65.19 inference(scs_inference,[],[49,44,66,86])). % 65.13/65.19 cnf(285,plain, % 65.13/65.19 (E(f16(x2851),f16(x2852))+~E(x2852,x2851)), % 65.13/65.19 inference(scs_inference,[],[2,4])). % 65.13/65.19 cnf(631,plain, % 65.13/65.19 (~E(x6311,x6312)+E(f12(x6312),f12(x6311))), % 65.13/65.19 inference(scs_inference,[],[23,2])). % 65.13/65.19 cnf(648,plain, % 65.13/65.19 (P1(x6481,f26(x6482))+~E(f17(x6482),x6481)), % 65.13/65.19 inference(scs_inference,[],[44,61,35])). % 65.13/65.19 cnf(649,plain, % 65.13/65.19 (P1(f17(x6491),f26(x6491))), % 65.13/65.19 inference(equality_inference,[],[648])). % 65.13/65.19 cnf(651,plain, % 65.13/65.19 (P1(f17(x6511),f26(x6511))), % 65.13/65.19 inference(rename_variables,[],[649])). % 65.13/65.19 cnf(654,plain, % 65.13/65.19 (P1(f17(x6541),f26(x6541))), % 65.13/65.19 inference(rename_variables,[],[649])). % 65.13/65.19 cnf(656,plain, % 65.13/65.19 (P1(f17(x6561),x6562)+~E(f26(x6561),x6562)), % 65.13/65.19 inference(scs_inference,[],[649,651,654,44,81,85,36])). % 65.13/65.19 cnf(1379,plain, % 65.13/65.19 (~E(f6(a1),f4(a3,a8,a10))+P3(f14(a9,a1),f24(a1))), % 65.13/65.19 inference(scs_inference,[],[186,2])). % 65.13/65.19 cnf(1491,plain, % 65.13/65.19 (~E(x14911,f4(a3,a8,a10))+~E(f6(a1),x14911)+P3(f14(a9,a1),f24(a1))), % 65.13/65.19 inference(scs_inference,[],[1379,3])). % 65.13/65.19 cnf(1764,plain, % 65.13/65.19 (~E(a8,x17641)+~P2(x17641)), % 65.13/65.19 inference(scs_inference,[],[49,40,2])). % 65.13/65.19 cnf(2171,plain, % 65.13/65.19 (P1(f13(x21711,x21711),f26(f5(x21711,x21711)))), % 65.13/65.19 inference(scs_inference,[],[44,72,84])). % 65.13/65.19 cnf(2172,plain, % 65.13/65.19 (P1(f13(x21721,x21721),f21(x21721,x21721))), % 65.13/65.19 inference(scs_inference,[],[44,2171,85])). % 65.13/65.19 cnf(3474,plain, % 65.13/65.19 (~P2(x34741)+P1(x34741,a2)), % 65.13/65.19 inference(scs_inference,[],[44,102,55])). % 65.13/65.19 cnf(3979,plain, % 65.13/65.19 (P1(f13(x39791,x39791),f21(x39791,x39791))), % 65.13/65.19 inference(rename_variables,[],[2172])). % 65.13/65.19 cnf(3981,plain, % 65.13/65.19 (E(f25(x39811,x39811,f13(x39811,x39811)),f24(f13(x39811,x39811)))), % 65.13/65.19 inference(scs_inference,[],[44,2172,3979,82,83])). % 65.13/65.19 cnf(3990,plain, % 65.13/65.19 (P1(f4(a3,a8,a10),f26(a3))+~P1(a3,a15)), % 65.13/65.19 inference(scs_inference,[],[46,44,3981,40,39,87])). % 65.13/65.19 cnf(3991,plain, % 65.13/65.19 (P1(x39911,a15)), % 65.13/65.19 inference(rename_variables,[],[44])). % 65.13/65.19 cnf(3993,plain, % 65.13/65.19 (P1(f25(a3,a8,a10),f26(a8))+~P1(a3,a15)), % 65.13/65.19 inference(scs_inference,[],[46,44,3991,3981,40,39,87,88])). % 65.13/65.19 cnf(3994,plain, % 65.13/65.19 (P1(x39941,a15)), % 65.13/65.19 inference(rename_variables,[],[44])). % 65.13/65.19 cnf(3996,plain, % 65.13/65.19 (E(f4(a3,a8,a10),f6(a10))+~P1(a3,a15)), % 65.13/65.19 inference(scs_inference,[],[46,44,3991,3994,3981,40,39,87,88,82])). % 65.13/65.19 cnf(3997,plain, % 65.13/65.19 (P1(x39971,a15)), % 65.13/65.19 inference(rename_variables,[],[44])). % 65.13/65.19 cnf(3999,plain, % 65.13/65.19 (E(f25(a3,a8,a10),f24(a10))+~P1(a3,a15)), % 65.13/65.19 inference(scs_inference,[],[46,44,3991,3994,3997,3981,40,39,87,88,82,83])). % 65.13/65.19 cnf(4012,plain, % 65.13/65.19 (P1(f4(a3,a8,a10),f26(a3))), % 65.13/65.19 inference(scs_inference,[],[44,3990])). % 65.13/65.19 cnf(4013,plain, % 65.13/65.19 (P1(f25(a3,a8,a10),f26(a8))), % 65.13/65.19 inference(scs_inference,[],[44,3993])). % 65.13/65.19 cnf(4014,plain, % 65.13/65.19 (E(f4(a3,a8,a10),f6(a10))), % 65.13/65.19 inference(scs_inference,[],[44,3996])). % 65.13/65.19 cnf(4015,plain, % 65.13/65.19 (E(f25(a3,a8,a10),f24(a10))), % 65.13/65.19 inference(scs_inference,[],[44,3999])). % 65.13/65.19 cnf(4021,plain, % 65.13/65.19 (P1(f24(a10),f26(a8))), % 65.13/65.19 inference(scs_inference,[],[4014,4015,4013,285,35])). % 65.13/65.19 cnf(4022,plain, % 65.13/65.19 (~P2(f4(a3,a8,a10))+P2(f6(a10))), % 65.13/65.19 inference(scs_inference,[],[4014,4015,4013,285,35,40])). % 65.13/65.19 cnf(4023,plain, % 65.13/65.19 (~P4(f25(a3,a8,a10))+P4(f24(a10))), % 65.13/65.19 inference(scs_inference,[],[4014,4015,4013,285,35,40,39])). % 65.13/65.19 cnf(4043,plain, % 65.13/65.19 (~P2(f25(a3,a8,a10))+P2(f24(a10))), % 65.13/65.19 inference(scs_inference,[],[4015,40])). % 65.13/65.19 cnf(4065,plain, % 65.13/65.19 (P2(f6(a10))+P3(f11(f4(a3,a8,a10)),f4(a3,a8,a10))), % 65.13/65.19 inference(scs_inference,[],[44,4022,59])). % 65.13/65.19 cnf(4081,plain, % 65.13/65.19 (~P2(f25(a3,a8,a10))+P4(f24(a10))), % 65.13/65.19 inference(scs_inference,[],[4023,102])). % 65.13/65.19 cnf(4097,plain, % 65.13/65.19 (P2(f24(a10))+P1(f12(f25(a3,a8,a10)),f16(f25(a3,a8,a10)))), % 65.13/65.19 inference(scs_inference,[],[44,4043,62])). % 65.13/65.19 cnf(4482,plain, % 65.13/65.19 (P1(x44821,f16(f25(a3,a8,a10)))+~E(f12(f25(a3,a8,a10)),x44821)+P2(f24(a10))), % 65.13/65.19 inference(scs_inference,[],[4097,35])). % 65.13/65.19 cnf(5685,plain, % 65.13/65.19 (~P3(f24(a10),f24(a10))+~P2(f25(a3,a8,a10))), % 65.13/65.19 inference(scs_inference,[],[193,4043])). % 65.13/65.19 cnf(6412,plain, % 65.13/65.19 (~P2(f25(a3,a8,a10))+~E(a8,f24(a10))), % 65.13/65.19 inference(scs_inference,[],[1764,4043])). % 65.13/65.19 cnf(6827,plain, % 65.13/65.19 (P1(f12(x68271),f16(x68271))+~E(a8,x68271)), % 65.13/65.19 inference(scs_inference,[],[44,1764,62])). % 65.13/65.19 cnf(6828,plain, % 65.13/65.19 (P1(f12(a8),f16(a8))), % 65.13/65.19 inference(equality_inference,[],[6827])). % 65.13/65.19 cnf(6830,plain, % 65.13/65.19 (P3(a8,a8)+~E(f12(a8),a8)), % 65.13/65.19 inference(scs_inference,[],[49,6828,44,35,67])). % 65.13/65.19 cnf(6850,plain, % 65.13/65.19 (~E(f12(a8),a8)+~P3(a8,f25(a3,a8,a10))), % 65.13/65.19 inference(scs_inference,[],[6830,240])). % 65.13/65.19 cnf(6866,plain, % 65.13/65.19 (~E(a8,f12(a8))+~P3(a8,f25(a3,a8,a10))), % 65.13/65.19 inference(scs_inference,[],[6850,2])). % 65.13/65.19 cnf(6882,plain, % 65.13/65.19 (~P3(x68821,f25(a3,a8,a10))+~E(x68821,a8)+~E(a8,f12(a8))), % 65.13/65.19 inference(scs_inference,[],[6866,37])). % 65.13/65.19 cnf(6898,plain, % 65.13/65.19 (P2(f25(a3,a8,a10))+~E(f11(f25(a3,a8,a10)),a8)+~E(a8,f12(a8))), % 65.13/65.19 inference(scs_inference,[],[44,6882,59])). % 65.13/65.19 cnf(7326,plain, % 65.13/65.19 (~P2(f25(a3,a8,a10))+P1(f24(a10),a2)), % 65.13/65.19 inference(scs_inference,[],[3474,4043])). % 65.13/65.19 cnf(7470,plain, % 65.13/65.19 (P1(x74701,a2)+P1(f12(x74701),f16(x74701))), % 65.13/65.19 inference(scs_inference,[],[44,3474,62])). % 65.13/65.19 cnf(7485,plain, % 65.13/65.19 (P3(a9,f6(a10))), % 65.13/65.19 inference(scs_inference,[],[47,4014,38])). % 65.13/65.19 cnf(7488,plain, % 65.13/65.19 (P1(a8,a2)+~P3(f12(a8),f25(a3,a8,a10))), % 65.13/65.19 inference(scs_inference,[],[7470,86])). % 65.13/65.19 cnf(7522,plain, % 65.13/65.19 (P1(f24(a10),x75221)+~E(f26(a8),x75221)), % 65.13/65.19 inference(scs_inference,[],[4021,36])). % 65.13/65.19 cnf(7557,plain, % 65.13/65.19 (P1(f12(a8),x75571)+~E(f16(a8),x75571)), % 65.13/65.19 inference(scs_inference,[],[6828,36])). % 65.13/65.19 cnf(7608,plain, % 65.13/65.19 (P1(f25(a3,a8,a10),x76081)+~E(f26(a8),x76081)), % 65.13/65.19 inference(scs_inference,[],[4013,36])). % 65.13/65.19 cnf(7683,plain, % 65.13/65.19 (P3(f14(a9,a10),f24(a10))+~P1(a10,a2)), % 65.13/65.19 inference(scs_inference,[],[44,7485,77])). % 65.13/65.19 cnf(7725,plain, % 65.13/65.19 (~P3(f12(a8),x77251)+~E(x77251,f25(a3,a8,a10))+P1(a8,a2)), % 65.13/65.19 inference(scs_inference,[],[7488,38])). % 65.13/65.19 cnf(7734,plain, % 65.13/65.19 (E(f6(a10),f4(a3,a8,a10))), % 65.13/65.19 inference(scs_inference,[],[4014,2])). % 65.13/65.19 cnf(7761,plain, % 65.13/65.19 (E(f24(a10),f25(a3,a8,a10))), % 65.13/65.19 inference(scs_inference,[],[4015,2])). % 65.13/65.19 cnf(7795,plain, % 65.13/65.19 (~P2(f24(a10))+P2(f25(a3,a8,a10))), % 65.13/65.19 inference(scs_inference,[],[7761,40])). % 65.13/65.19 cnf(7819,plain, % 65.13/65.19 (~P3(f12(a8),f25(a3,a8,a10))), % 65.13/65.19 inference(scs_inference,[],[6828,86])). % 65.13/65.19 cnf(7913,plain, % 65.13/65.19 (~P3(f25(a3,a8,a10),f25(a3,a8,a10))+~P2(f24(a10))), % 65.13/65.19 inference(scs_inference,[],[7795,193])). % 65.13/65.19 cnf(8898,plain, % 65.13/65.19 (~P3(f24(a10),f25(a3,a8,a10))+~P2(f24(a10))), % 65.13/65.19 inference(scs_inference,[],[7761,7913,37])). % 65.13/65.19 cnf(8914,plain, % 65.13/65.19 (~P2(f25(a3,a8,a10))+~P3(f24(a10),f25(a3,a8,a10))), % 65.13/65.19 inference(scs_inference,[],[8898,4043])). % 65.13/65.19 cnf(9755,plain, % 65.13/65.19 (~P2(f22(x97551))), % 65.13/65.19 inference(scs_inference,[],[44,51])). % 65.13/65.19 cnf(9788,plain, % 65.13/65.19 (~P3(f12(a8),f24(a10))), % 65.13/65.19 inference(scs_inference,[],[7819,7734,7761,44,51,631,10,11,12,15,16,19,20,23,5,6,13,14,17,18,21,22,27,28,29,30,31,32,33,34,7,8,9,24,25,26,38])). % 65.13/65.19 cnf(9818,plain, % 65.13/65.19 (~P3(f25(a3,a8,a10),x98181)+P3(f24(a10),x98181)), % 65.13/65.19 inference(scs_inference,[],[4015,7734,1491,37])). % 65.13/65.19 cnf(9819,plain, % 65.13/65.19 (P1(f12(a3),f16(a3))), % 65.13/65.19 inference(scs_inference,[],[48,44,62])). % 65.13/65.19 cnf(9820,plain, % 65.13/65.19 (P1(x98201,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(9822,plain, % 65.13/65.20 (~P3(x98221,f24(a10))+~E(x98221,f12(a8))), % 65.13/65.20 inference(scs_inference,[],[9788,48,44,62,37])). % 65.13/65.20 cnf(9823,plain, % 65.13/65.20 (~E(f14(a9,a10),f12(a8))+~P1(a10,a2)), % 65.13/65.20 inference(scs_inference,[],[9788,7485,48,44,9820,62,37,77])). % 65.13/65.20 cnf(9840,plain, % 65.13/65.20 (~P3(f4(a3,a8,a10),x98401)+P3(f6(a10),x98401)), % 65.13/65.20 inference(scs_inference,[],[4014,37])). % 65.13/65.20 cnf(9848,plain, % 65.13/65.20 (~P3(x98481,f25(a3,a8,a10))+~E(x98481,f12(a8))), % 65.13/65.20 inference(scs_inference,[],[7819,37])). % 65.13/65.20 cnf(9860,plain, % 65.13/65.20 (P3(f11(a3),a3)), % 65.13/65.20 inference(scs_inference,[],[48,44,59])). % 65.13/65.20 cnf(9863,plain, % 65.13/65.20 (~P3(f24(a10),x98631)+P3(f25(a3,a8,a10),x98631)), % 65.13/65.20 inference(scs_inference,[],[48,7761,44,59,37])). % 65.13/65.20 cnf(9885,plain, % 65.13/65.20 (P1(a10,f26(f5(a3,a8)))), % 65.13/65.20 inference(scs_inference,[],[46,44,84,141])). % 65.13/65.20 cnf(9891,plain, % 65.13/65.20 (P1(f4(a3,a8,a10),f16(f22(a3)))), % 65.13/65.20 inference(scs_inference,[],[4012,44,71,141])). % 65.13/65.20 cnf(9894,plain, % 65.13/65.20 (P1(f6(a10),f16(f22(a3)))), % 65.13/65.20 inference(scs_inference,[],[9891,4014,35])). % 65.13/65.20 cnf(9895,plain, % 65.13/65.20 (P3(x98951,f22(x98951))+~P3(f18(x98951,x98951),x98951)), % 65.13/65.20 inference(scs_inference,[],[9891,4014,44,35,78])). % 65.13/65.20 cnf(9924,plain, % 65.13/65.20 (P1(f11(a3),f16(a3))+~P1(a3,a15)), % 65.13/65.20 inference(scs_inference,[],[9860,48,44,66])). % 65.13/65.20 cnf(9930,plain, % 65.13/65.20 (P1(x99301,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(9931,plain, % 65.13/65.20 (P3(f6(a10),f22(a3))+~P1(f22(a3),a15)), % 65.13/65.20 inference(scs_inference,[],[9894,9755,44,9930,9924,67])). % 65.13/65.20 cnf(9938,plain, % 65.13/65.20 (P1(x99381,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(9939,plain, % 65.13/65.20 (P3(f4(a3,a8,a10),f22(a3))), % 65.13/65.20 inference(scs_inference,[],[7734,44,9931,37])). % 65.13/65.20 cnf(9942,plain, % 65.13/65.20 (~P1(f25(a3,a8,a10),a15)+P1(f25(a3,a8,a10),f16(f22(a8)))), % 65.13/65.20 inference(scs_inference,[],[4013,7734,44,9938,9931,37,76,71])). % 65.13/65.20 cnf(9945,plain, % 65.13/65.20 (P1(f25(a3,a8,a10),f16(f22(a8)))), % 65.13/65.20 inference(scs_inference,[],[44,9942])). % 65.13/65.20 cnf(9948,plain, % 65.13/65.20 (~E(x99481,a8)+~P2(x99481)), % 65.13/65.20 inference(scs_inference,[],[49,4014,44,9942,36,40])). % 65.13/65.20 cnf(9950,plain, % 65.13/65.20 (P1(f24(a10),f16(f22(a8)))), % 65.13/65.20 inference(scs_inference,[],[9945,4015,35])). % 65.13/65.20 cnf(9951,plain, % 65.13/65.20 (~P2(f6(a10))+~P1(a9,a15)), % 65.13/65.20 inference(scs_inference,[],[9945,7485,4015,44,35,63])). % 65.13/65.20 cnf(9954,plain, % 65.13/65.20 (~P2(f6(a10))), % 65.13/65.20 inference(scs_inference,[],[44,9951])). % 65.13/65.20 cnf(9955,plain, % 65.13/65.20 (P1(x99551,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(9956,plain, % 65.13/65.20 (P3(f11(f6(a10)),f6(a10))), % 65.13/65.20 inference(scs_inference,[],[44,9955,9951,59])). % 65.13/65.20 cnf(9957,plain, % 65.13/65.20 (P1(x99571,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(9959,plain, % 65.13/65.20 (P3(f24(a10),f22(a8))+~P1(f22(a8),a15)), % 65.13/65.20 inference(scs_inference,[],[9950,9755,44,9955,9957,9951,59,67])). % 65.13/65.20 cnf(9965,plain, % 65.13/65.20 (~P2(f4(a3,a8,a10))), % 65.13/65.20 inference(scs_inference,[],[9954,4022])). % 65.13/65.20 cnf(9966,plain, % 65.13/65.20 (P3(f11(f4(a3,a8,a10)),f4(a3,a8,a10))), % 65.13/65.20 inference(scs_inference,[],[9954,4065])). % 65.13/65.20 cnf(9972,plain, % 65.13/65.20 (P3(f25(a3,a8,a10),f22(a8))), % 65.13/65.20 inference(scs_inference,[],[9956,7734,44,9959,38,9863])). % 65.13/65.20 cnf(9995,plain, % 65.13/65.20 (P3(f12(a3),a3)+~P1(a3,a15)), % 65.13/65.20 inference(scs_inference,[],[9819,48,44,67])). % 65.13/65.20 cnf(10000,plain, % 65.13/65.20 (P1(x100001,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10005,plain, % 65.13/65.20 (P1(f17(x100051),f16(f22(x100051)))), % 65.13/65.20 inference(scs_inference,[],[649,44,10000,9995,71,656,141])). % 65.13/65.20 cnf(10009,plain, % 65.13/65.20 (P2(f24(a10))+~P1(f12(a8),f16(f24(a10)))+~P1(f24(a10),a15)), % 65.13/65.20 inference(scs_inference,[],[9788,44,67])). % 65.13/65.20 cnf(10019,plain, % 65.13/65.20 (~P1(f12(a8),f16(f24(a10)))+P2(f24(a10))), % 65.13/65.20 inference(scs_inference,[],[44,10009])). % 65.13/65.20 cnf(10029,plain, % 65.13/65.20 (P3(f17(x100291),f22(x100291))+~P1(f22(x100291),a15)), % 65.13/65.20 inference(scs_inference,[],[10005,9755,44,67])). % 65.13/65.20 cnf(10041,plain, % 65.13/65.20 (P3(f17(x100411),f22(x100411))), % 65.13/65.20 inference(scs_inference,[],[44,10029])). % 65.13/65.20 cnf(10042,plain, % 65.13/65.20 (P1(x100421,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10045,plain, % 65.13/65.20 (P2(f25(a3,a8,a10))+~P1(f12(a8),f16(f25(a3,a8,a10)))+~P1(f25(a3,a8,a10),a15)), % 65.13/65.20 inference(scs_inference,[],[7819,44,10042,10029,67])). % 65.13/65.20 cnf(10047,plain, % 65.13/65.20 (P1(x100471,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10062,plain, % 65.13/65.20 (~P1(f12(a8),f16(f25(a3,a8,a10)))+P2(f24(a10))), % 65.13/65.20 inference(scs_inference,[],[9965,44,10047,10045,40,63,1764,3474,9948,4081,6412,7326,5685,8914,9818,4043])). % 65.13/65.20 cnf(10086,plain, % 65.13/65.20 (P3(f12(a8),a8)+~P1(a8,a15)), % 65.13/65.20 inference(scs_inference,[],[6828,49,44,67])). % 65.13/65.20 cnf(10087,plain, % 65.13/65.20 (P1(x100871,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10090,plain, % 65.13/65.20 (P3(f11(f4(a3,a8,a10)),a3)+~P1(f4(a3,a8,a10),a15)+~P1(f11(f4(a3,a8,a10)),a15)), % 65.13/65.20 inference(scs_inference,[],[9966,9939,6828,49,44,10087,79])). % 65.13/65.20 cnf(10092,plain, % 65.13/65.20 (P3(f12(a8),a8)), % 65.13/65.20 inference(scs_inference,[],[44,10086])). % 65.13/65.20 cnf(10093,plain, % 65.13/65.20 (P1(x100931,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10095,plain, % 65.13/65.20 (P1(x100951,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10096,plain, % 65.13/65.20 (P3(f11(f4(a3,a8,a10)),a3)), % 65.13/65.20 inference(scs_inference,[],[44,10093,10095,10086,10090,36])). % 65.13/65.20 cnf(10103,plain, % 65.13/65.20 (~P1(f25(a3,a8,a10),a15)+~P1(f12(a8),a15)+~P3(a8,f22(f25(a3,a8,a10)))), % 65.13/65.20 inference(scs_inference,[],[10092,7819,44,79])). % 65.13/65.20 cnf(10105,plain, % 65.13/65.20 (P1(x101051,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10108,plain, % 65.13/65.20 (~P3(a8,f22(f25(a3,a8,a10)))), % 65.13/65.20 inference(scs_inference,[],[7761,44,10105,10103,35,7608,141])). % 65.13/65.20 cnf(10111,plain, % 65.13/65.20 (~E(f17(f25(a3,a8,a10)),a8)), % 65.13/65.20 inference(scs_inference,[],[10108,10041,37])). % 65.13/65.20 cnf(10117,plain, % 65.13/65.20 (~P3(f18(a8,f25(a3,a8,a10)),f25(a3,a8,a10))), % 65.13/65.20 inference(scs_inference,[],[10108,10041,44,37,78,7608,141])). % 65.13/65.20 cnf(10121,plain, % 65.13/65.20 (~P3(f18(a8,f25(a3,a8,a10)),f24(a10))), % 65.13/65.20 inference(scs_inference,[],[10117,10111,7761,2,38])). % 65.13/65.20 cnf(10122,plain, % 65.13/65.20 (~P1(f25(a3,a8,a10),a15)+P3(f18(a8,f25(a3,a8,a10)),a8)), % 65.13/65.20 inference(scs_inference,[],[10117,10111,10108,7761,44,2,38,70])). % 65.13/65.20 cnf(10123,plain, % 65.13/65.20 (P1(x101231,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10127,plain, % 65.13/65.20 (P1(f11(f4(a3,a8,a10)),f16(a3))+~P1(a3,a15)), % 65.13/65.20 inference(scs_inference,[],[10117,10111,10096,10092,10108,48,7761,44,10123,2,38,70,7725,66])). % 65.13/65.20 cnf(10131,plain, % 65.13/65.20 (P1(x101311,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10132,plain, % 65.13/65.20 (P3(f18(a8,f25(a3,a8,a10)),a8)), % 65.13/65.20 inference(scs_inference,[],[44,10131,10127,10122])). % 65.13/65.20 cnf(10161,plain, % 65.13/65.20 (~P3(a8,x101611)+~E(x101611,f22(f25(a3,a8,a10)))), % 65.13/65.20 inference(scs_inference,[],[10108,9965,47,44,66,38])). % 65.13/65.20 cnf(10175,plain, % 65.13/65.20 (~P3(x101751,f24(a10))+~E(x101751,f18(a8,f25(a3,a8,a10)))), % 65.13/65.20 inference(scs_inference,[],[10121,37])). % 65.13/65.20 cnf(10201,plain, % 65.13/65.20 (P1(x102011,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10204,plain, % 65.13/65.20 (~P1(f24(a10),a15)+~P3(a8,f22(f24(a10)))+~P1(f18(a8,f25(a3,a8,a10)),a15)), % 65.13/65.20 inference(scs_inference,[],[10132,10121,44,10201,79])). % 65.13/65.20 cnf(10206,plain, % 65.13/65.20 (P1(x102061,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10210,plain, % 65.13/65.20 (~P3(a8,f22(f24(a10)))), % 65.13/65.20 inference(scs_inference,[],[9950,4015,44,10206,10204,36,35,7522,141])). % 65.13/65.20 cnf(10213,plain, % 65.13/65.20 (~P3(a8,x102131)+~E(x102131,f22(f24(a10)))), % 65.13/65.20 inference(scs_inference,[],[10210,38])). % 65.13/65.20 cnf(10219,plain, % 65.13/65.20 (~P1(f24(a10),a15)+P3(f18(a8,f24(a10)),a8)), % 65.13/65.20 inference(scs_inference,[],[10210,44,70])). % 65.13/65.20 cnf(10220,plain, % 65.13/65.20 (P1(x102201,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10222,plain, % 65.13/65.20 (~P3(f18(a8,f24(a10)),f24(a10))+~P1(a8,a15)), % 65.13/65.20 inference(scs_inference,[],[10210,44,10220,70,78])). % 65.13/65.20 cnf(10227,plain, % 65.13/65.20 (P1(x102271,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10228,plain, % 65.13/65.20 (~P3(f18(a8,f24(a10)),f24(a10))), % 65.13/65.20 inference(scs_inference,[],[44,10227,10219,10222])). % 65.13/65.20 cnf(10763,plain, % 65.13/65.20 (P3(x107631,f22(x107631))), % 65.13/65.20 inference(scs_inference,[],[9895,195])). % 65.13/65.20 cnf(10766,plain, % 65.13/65.20 (P3(x107661,f22(x107661))), % 65.13/65.20 inference(rename_variables,[],[10763])). % 65.13/65.20 cnf(10767,plain, % 65.13/65.20 (~E(f22(f25(a3,a8,a10)),f22(a8))), % 65.13/65.20 inference(scs_inference,[],[10763,10161,2])). % 65.13/65.20 cnf(10769,plain, % 65.13/65.20 (P3(x107691,f22(x107691))), % 65.13/65.20 inference(rename_variables,[],[10763])). % 65.13/65.20 cnf(10771,plain, % 65.13/65.20 (P3(x107711,f22(x107711))), % 65.13/65.20 inference(rename_variables,[],[10763])). % 65.13/65.20 cnf(10772,plain, % 65.13/65.20 (~E(f22(a8),f22(f24(a10)))), % 65.13/65.20 inference(scs_inference,[],[10763,10766,10769,10771,4015,10161,2,9840,37,10213])). % 65.13/65.20 cnf(10773,plain, % 65.13/65.20 (P3(x107731,f22(x107731))), % 65.13/65.20 inference(rename_variables,[],[10763])). % 65.13/65.20 cnf(10774,plain, % 65.13/65.20 (P3(f25(a3,a8,a10),f22(f24(a10)))), % 65.13/65.20 inference(scs_inference,[],[10763,10766,10769,10771,10773,4015,10161,2,9840,37,10213,9863])). % 65.13/65.20 cnf(10780,plain, % 65.13/65.20 (~E(f25(a3,a8,a10),a8)), % 65.13/65.20 inference(scs_inference,[],[10774,10772,10210,2,37])). % 65.13/65.20 cnf(10792,plain, % 65.13/65.20 (P1(x107921,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10794,plain, % 65.13/65.20 (P1(x107941,f26(x107941))+~P1(f22(x107941),a15)), % 65.13/65.20 inference(scs_inference,[],[10780,10763,9755,7761,44,10792,2,3,66,76])). % 65.13/65.20 cnf(10799,plain, % 65.13/65.20 (P1(x107991,f26(x107991))), % 65.13/65.20 inference(scs_inference,[],[44,10794])). % 65.13/65.20 cnf(10814,plain, % 65.13/65.20 (P1(x108141,f26(x108141))), % 65.13/65.20 inference(rename_variables,[],[10799])). % 65.13/65.20 cnf(10816,plain, % 65.13/65.20 (P1(f5(x108161,x108161),f21(x108161,x108161))), % 65.13/65.20 inference(scs_inference,[],[10799,10814,44,81,85])). % 65.13/65.20 cnf(10834,plain, % 65.13/65.20 (P1(x108341,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10837,plain, % 65.13/65.20 (P1(x108371,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10838,plain, % 65.13/65.20 (P1(x108381,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10843,plain, % 65.13/65.20 (P4(a10)), % 65.13/65.20 inference(scs_inference,[],[10816,9885,10767,44,10834,10838,10837,88,87,72,3,81])). % 65.13/65.20 cnf(10878,plain, % 65.13/65.20 (P1(a10,a2)), % 65.13/65.20 inference(scs_inference,[],[10843,44,55])). % 65.13/65.20 cnf(10883,plain, % 65.13/65.20 (P3(f14(a9,a10),f24(a10))), % 65.13/65.20 inference(scs_inference,[],[10878,7683])). % 65.13/65.20 cnf(10884,plain, % 65.13/65.20 (~E(f14(a9,a10),f12(a8))), % 65.13/65.20 inference(scs_inference,[],[10878,9823])). % 65.13/65.20 cnf(10888,plain, % 65.13/65.20 (~E(f14(a9,a10),f18(a8,f24(a10)))), % 65.13/65.20 inference(scs_inference,[],[10883,10884,10228,2,37])). % 65.13/65.20 cnf(10889,plain, % 65.13/65.20 (~E(f14(a9,a10),f18(a8,f25(a3,a8,a10)))), % 65.13/65.20 inference(scs_inference,[],[10883,10884,10228,2,37,10175])). % 65.13/65.20 cnf(10890,plain, % 65.13/65.20 (~P2(f24(a10))+~P1(f14(a9,a10),a15)), % 65.13/65.20 inference(scs_inference,[],[10883,10884,10228,44,2,37,10175,63])). % 65.13/65.20 cnf(10893,plain, % 65.13/65.20 (~P1(f12(a8),f16(f24(a10)))+~P1(f14(a9,a10),a15)), % 65.13/65.20 inference(scs_inference,[],[10883,10884,10228,44,2,37,10175,63,10019])). % 65.13/65.20 cnf(10894,plain, % 65.13/65.20 (~E(a15,f16(f24(a10)))+~P1(f14(a9,a10),a15)), % 65.13/65.20 inference(scs_inference,[],[10883,10884,10228,44,2,37,10175,63,10019,141])). % 65.13/65.20 cnf(10898,plain, % 65.13/65.20 (~P2(f24(a10))), % 65.13/65.20 inference(scs_inference,[],[10889,44,2,10890])). % 65.13/65.20 cnf(10899,plain, % 65.13/65.20 (P1(x108991,a15)), % 65.13/65.20 inference(rename_variables,[],[44])). % 65.13/65.20 cnf(10901,plain, % 65.24/65.20 (P1(x109011,a15)), % 65.24/65.20 inference(rename_variables,[],[44])). % 65.24/65.20 cnf(10903,plain, % 65.24/65.20 (P1(x109031,a15)), % 65.24/65.20 inference(rename_variables,[],[44])). % 65.24/65.20 cnf(10904,plain, % 65.24/65.20 (~P2(f25(a3,a8,a10))), % 65.24/65.20 inference(scs_inference,[],[10889,4015,44,10899,10901,2,10890,10894,10893,40])). % 65.24/65.20 cnf(10906,plain, % 65.24/65.20 (~P1(f12(a8),f16(f25(a3,a8,a10)))), % 65.24/65.20 inference(scs_inference,[],[10889,4015,44,10899,10901,2,10890,10894,10893,40,7557,10062])). % 65.24/65.20 cnf(10909,plain, % 65.24/65.20 (P3(f11(f24(a10)),f24(a10))), % 65.24/65.20 inference(scs_inference,[],[10889,4015,44,10899,10901,10903,2,10890,10894,10893,40,7557,10062,141,6898,59])). % 65.24/65.20 cnf(10915,plain, % 65.24/65.20 (~E(f12(f25(a3,a8,a10)),x109151)+P1(x109151,f16(f25(a3,a8,a10)))), % 65.24/65.20 inference(scs_inference,[],[10898,4482])). % 65.24/65.20 cnf(10925,plain, % 65.24/65.20 (P3(f11(f25(a3,a8,a10)),f25(a3,a8,a10))), % 65.24/65.20 inference(scs_inference,[],[10904,10888,10906,44,10915,7557,2,59])). % 65.24/65.20 cnf(10930,plain, % 65.24/65.20 (~P1(f11(f25(a3,a8,a10)),f16(a8))), % 65.24/65.20 inference(scs_inference,[],[10904,10909,10888,10906,44,10915,7557,2,59,9848,9822,86])). % 65.24/65.20 cnf(10932,plain, % 65.24/65.20 (~E(a15,f16(a8))), % 65.24/65.20 inference(scs_inference,[],[10904,10909,10888,10906,44,10915,7557,2,59,9848,9822,86,141])). % 65.24/65.20 cnf(10941,plain, % 65.24/65.20 (P1(x109411,a15)), % 65.24/65.20 inference(rename_variables,[],[44])). % 65.24/65.20 cnf(10943,plain, % 65.24/65.20 (~P1(a8,a15)+~P1(f11(f25(a3,a8,a10)),a15)), % 65.24/65.20 inference(scs_inference,[],[10932,10930,10925,9972,49,44,10941,2,66,79])). % 65.24/65.20 cnf(10946,plain, % 65.24/65.20 (~P1(a8,a15)), % 65.24/65.20 inference(scs_inference,[],[44,10943])). % 65.24/65.20 cnf(10958,plain, % 65.24/65.20 ($false), % 65.24/65.20 inference(scs_inference,[],[10946,44]), % 65.24/65.20 ['proof']). % 65.24/65.20 % SZS output end Proof % 65.24/65.20 % Total time :64.530000s %------------------------------------------------------------------------------