%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS098+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n013.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 10:08:29 EDT 2024 % Result : Unsatisfiable 1.93s 2.00s % Output : CNFRefutation 1.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : KRS098+1 : TPTP v8.2.0. Released v3.1.0. % 0.04/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.36 % Computer : n013.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Wed Jun 19 14:30:09 EDT 2024 % 0.14/0.36 % CPUTime : % 0.52/0.60 start to proof:theBenchmark % 1.93/1.99 %------------------------------------------- % 1.93/1.99 % File :CSE---1.7 % 1.93/1.99 % Problem :theBenchmark % 1.93/1.99 % Transform :cnf % 1.93/1.99 % Format :tptp:raw % 1.93/1.99 % Command :java -jar mcs_scs.jar %d %s % 1.93/1.99 % 1.93/1.99 % Result :Theorem 1.340000s % 1.93/1.99 % Output :CNFRefutation 1.340000s % 1.93/1.99 %------------------------------------------- % 1.93/1.99 %------------------------------------------------------------------------------ % 1.93/1.99 % File : KRS098+1 : TPTP v8.2.0. Released v3.1.0. % 1.93/1.99 % Domain : Knowledge Representation (Semantic Web) % 1.93/1.99 % Problem : DL Test: heinsohn3.2 % 1.93/2.00 % Version : Especial. % 1.93/2.00 % English : Tbox tests from [HK+94] % 1.93/2.00 % 1.93/2.00 % Refs : [HK+94] Heinsohn et al. (1994), An Empirical Analysis of Termi % 1.93/2.00 % : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 1.93/2.00 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 1.93/2.00 % Source : [Bec03] % 1.93/2.00 % Names : inconsistent_description-logic-Manifest108 [Bec03] % 1.93/2.00 % 1.93/2.00 % Status : Unsatisfiable % 1.93/2.00 % Rating : 0.14 v8.2.0, 0.00 v3.1.0 % 1.93/2.00 % Syntax : Number of formulae : 39 ( 1 unt; 0 def) % 1.93/2.00 % Number of atoms : 123 ( 29 equ) % 1.93/2.00 % Maximal formula atoms : 22 ( 3 avg) % 1.93/2.00 % Number of connectives : 91 ( 7 ~; 1 |; 46 &) % 1.93/2.00 % ( 3 <=>; 34 =>; 0 <=; 0 <~>) % 1.93/2.00 % Maximal formula depth : 13 ( 5 avg) % 1.93/2.00 % Maximal term depth : 1 ( 1 avg) % 1.93/2.00 % Number of predicates : 18 ( 17 usr; 0 prp; 1-2 aty) % 1.93/2.00 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 1.93/2.00 % Number of variables : 99 ( 91 !; 8 ?) % 1.93/2.00 % SPC : FOF_UNS_RFO_SEQ % 1.93/2.00 % 1.93/2.00 % Comments : Sean Bechhofer says there are some errors in the encoding of % 1.93/2.00 % datatypes, so this problem may not be perfect. At least it's % 1.93/2.00 % still representative of the type of reasoning required for OWL. % 1.93/2.00 % : Tests incoherency caused by number restrictions and role hierarchy % 1.93/2.00 %------------------------------------------------------------------------------ % 1.93/2.00 fof(cUnsatisfiable_substitution_1,axiom, % 1.93/2.00 ! [A,B] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & cUnsatisfiable(A) ) % 1.93/2.00 => cUnsatisfiable(B) ) ). % 1.93/2.00 % 1.93/2.00 fof(ca_substitution_1,axiom, % 1.93/2.00 ! [A,B] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & ca(A) ) % 1.93/2.00 => ca(B) ) ). % 1.93/2.00 % 1.93/2.00 fof(cc_substitution_1,axiom, % 1.93/2.00 ! [A,B] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & cc(A) ) % 1.93/2.00 => cc(B) ) ). % 1.93/2.00 % 1.93/2.00 fof(cd_substitution_1,axiom, % 1.93/2.00 ! [A,B] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & cd(A) ) % 1.93/2.00 => cd(B) ) ). % 1.93/2.00 % 1.93/2.00 fof(ce_substitution_1,axiom, % 1.93/2.00 ! [A,B] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & ce(A) ) % 1.93/2.00 => ce(B) ) ). % 1.93/2.00 % 1.93/2.00 fof(cowlNothing_substitution_1,axiom, % 1.93/2.00 ! [A,B] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & cowlNothing(A) ) % 1.93/2.00 => cowlNothing(B) ) ). % 1.93/2.00 % 1.93/2.00 fof(cowlThing_substitution_1,axiom, % 1.93/2.00 ! [A,B] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & cowlThing(A) ) % 1.93/2.00 => cowlThing(B) ) ). % 1.93/2.00 % 1.93/2.00 fof(rr_substitution_1,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rr(A,C) ) % 1.93/2.00 => rr(B,C) ) ). % 1.93/2.00 % 1.93/2.00 fof(rr_substitution_2,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rr(C,A) ) % 1.93/2.00 => rr(C,B) ) ). % 1.93/2.00 % 1.93/2.00 fof(rr1_substitution_1,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rr1(A,C) ) % 1.93/2.00 => rr1(B,C) ) ). % 1.93/2.00 % 1.93/2.00 fof(rr1_substitution_2,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rr1(C,A) ) % 1.93/2.00 => rr1(C,B) ) ). % 1.93/2.00 % 1.93/2.00 fof(rr2_substitution_1,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rr2(A,C) ) % 1.93/2.00 => rr2(B,C) ) ). % 1.93/2.00 % 1.93/2.00 fof(rr2_substitution_2,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rr2(C,A) ) % 1.93/2.00 => rr2(C,B) ) ). % 1.93/2.00 % 1.93/2.00 fof(rr3_substitution_1,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rr3(A,C) ) % 1.93/2.00 => rr3(B,C) ) ). % 1.93/2.00 % 1.93/2.00 fof(rr3_substitution_2,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rr3(C,A) ) % 1.93/2.00 => rr3(C,B) ) ). % 1.93/2.00 % 1.93/2.00 fof(rt1_substitution_1,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rt1(A,C) ) % 1.93/2.00 => rt1(B,C) ) ). % 1.93/2.00 % 1.93/2.00 fof(rt1_substitution_2,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rt1(C,A) ) % 1.93/2.00 => rt1(C,B) ) ). % 1.93/2.00 % 1.93/2.00 fof(rt2_substitution_1,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rt2(A,C) ) % 1.93/2.00 => rt2(B,C) ) ). % 1.93/2.00 % 1.93/2.00 fof(rt2_substitution_2,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rt2(C,A) ) % 1.93/2.00 => rt2(C,B) ) ). % 1.93/2.00 % 1.93/2.00 fof(rt3_substitution_1,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rt3(A,C) ) % 1.93/2.00 => rt3(B,C) ) ). % 1.93/2.00 % 1.93/2.00 fof(rt3_substitution_2,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rt3(C,A) ) % 1.93/2.00 => rt3(C,B) ) ). % 1.93/2.00 % 1.93/2.00 fof(rtt_substitution_1,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rtt(A,C) ) % 1.93/2.00 => rtt(B,C) ) ). % 1.93/2.00 % 1.93/2.00 fof(rtt_substitution_2,axiom, % 1.93/2.00 ! [A,B,C] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & rtt(C,A) ) % 1.93/2.00 => rtt(C,B) ) ). % 1.93/2.00 % 1.93/2.00 fof(xsd_integer_substitution_1,axiom, % 1.93/2.00 ! [A,B] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & xsd_integer(A) ) % 1.93/2.00 => xsd_integer(B) ) ). % 1.93/2.00 % 1.93/2.00 fof(xsd_string_substitution_1,axiom, % 1.93/2.00 ! [A,B] : % 1.93/2.00 ( ( A = B % 1.93/2.00 & xsd_string(A) ) % 1.93/2.00 => xsd_string(B) ) ). % 1.93/2.00 % 1.93/2.00 %----Thing and Nothing % 1.93/2.00 fof(axiom_0,axiom, % 1.93/2.00 ! [X] : % 1.93/2.00 ( cowlThing(X) % 1.93/2.00 & ~ cowlNothing(X) ) ). % 1.93/2.00 % 1.93/2.00 %----String and Integer disjoint % 1.93/2.00 fof(axiom_1,axiom, % 1.93/2.00 ! [X] : % 1.93/2.00 ( xsd_string(X) % 1.93/2.00 <=> ~ xsd_integer(X) ) ). % 1.93/2.00 % 1.93/2.00 %----Equality cUnsatisfiable % 1.93/2.00 fof(axiom_2,axiom, % 1.93/2.00 ! [X] : % 1.93/2.00 ( cUnsatisfiable(X) % 1.93/2.00 <=> ( ? [Y] : % 1.93/2.00 ( rr3(X,Y) % 1.93/2.00 & ? [Z] : % 1.93/2.00 ( rt3(Y,Z) % 1.93/2.00 & ce(Z) ) % 1.93/2.00 & ! [Z0,Z1] : % 1.93/2.00 ( ( rtt(Y,Z0) % 1.93/2.00 & rtt(Y,Z1) ) % 1.93/2.00 => Z0 = Z1 ) ) % 1.93/2.00 & ? [Y] : % 1.93/2.00 ( rr2(X,Y) % 1.93/2.00 & ! [Z0,Z1] : % 1.93/2.00 ( ( rtt(Y,Z0) % 1.93/2.00 & rtt(Y,Z1) ) % 1.93/2.00 => Z0 = Z1 ) % 1.93/2.00 & ? [Z] : % 1.93/2.00 ( rt2(Y,Z) % 1.93/2.00 & cd(Z) ) ) % 1.93/2.00 & ~ ? [Y0,Y1] : % 1.93/2.00 ( rr(X,Y0) % 1.93/2.00 & rr(X,Y1) % 1.93/2.00 & Y0 != Y1 ) % 1.93/2.00 & ? [Y] : % 1.93/2.00 ( rr1(X,Y) % 1.93/2.00 & ! [Z0,Z1] : % 1.93/2.00 ( ( rtt(Y,Z0) % 1.93/2.00 & rtt(Y,Z1) ) % 1.93/2.00 => Z0 = Z1 ) % 1.93/2.00 & ? [Z] : % 1.93/2.00 ( rt1(Y,Z) % 1.93/2.00 & cc(Z) ) ) ) ) ). % 1.93/2.00 % 1.93/2.00 %----Equality ca % 1.93/2.00 fof(axiom_3,axiom, % 1.93/2.00 ! [X] : % 1.93/2.00 ( ca(X) % 1.93/2.00 <=> ( cc(X) % 1.93/2.00 | cd(X) ) ) ). % 1.93/2.00 % 1.93/2.00 %----i2003_11_14_17_20_25524 % 1.93/2.00 fof(axiom_4,axiom, % 1.93/2.00 cUnsatisfiable(i2003_11_14_17_20_25524) ). % 1.93/2.00 % 1.93/2.00 fof(axiom_5,axiom, % 1.93/2.00 ! [X] : % 1.93/2.00 ~ ( cc(X) % 1.93/2.00 & cd(X) ) ). % 1.93/2.00 % 1.93/2.00 fof(axiom_6,axiom, % 1.93/2.00 ! [X] : % 1.93/2.00 ~ ( ce(X) % 1.93/2.00 & cc(X) ) ). % 1.93/2.00 % 1.93/2.00 fof(axiom_7,axiom, % 1.93/2.00 ! [X] : % 1.93/2.00 ~ ( ce(X) % 1.93/2.00 & cd(X) ) ). % 1.93/2.00 % 1.93/2.00 fof(axiom_8,axiom, % 1.93/2.00 ! [X,Y] : % 1.93/2.00 ( rr1(X,Y) % 1.93/2.00 => rr(X,Y) ) ). % 1.93/2.00 % 1.93/2.00 fof(axiom_9,axiom, % 1.93/2.00 ! [X,Y] : % 1.93/2.00 ( rr2(X,Y) % 1.93/2.00 => rr(X,Y) ) ). % 1.93/2.00 % 1.93/2.00 fof(axiom_10,axiom, % 1.93/2.00 ! [X,Y] : % 1.93/2.00 ( rt1(X,Y) % 1.93/2.00 => rtt(X,Y) ) ). % 1.93/2.00 % 1.93/2.00 fof(axiom_11,axiom, % 1.93/2.00 ! [X,Y] : % 1.93/2.00 ( rt2(X,Y) % 1.93/2.00 => rtt(X,Y) ) ). % 1.93/2.00 % 1.93/2.00 fof(axiom_12,axiom, % 1.93/2.00 ! [X,Y] : % 1.93/2.00 ( rr3(X,Y) % 1.93/2.00 => rr(X,Y) ) ). % 1.93/2.00 % 1.93/2.00 fof(axiom_13,axiom, % 1.93/2.00 ! [X,Y] : % 1.93/2.00 ( rt3(X,Y) % 1.93/2.00 => rtt(X,Y) ) ). % 1.93/2.00 % 1.93/2.00 %------------------------------------------------------------------------------ % 1.93/2.00 %------------------------------------------- % 1.93/2.00 % Proof found % 1.93/2.00 % SZS status Theorem for theBenchmark % 1.93/2.00 % SZS output start Proof % 1.93/2.00 %ClaNum:108(EqnAxiom:48) % 1.93/2.00 %VarNum:658(SingletonVarNum:187) % 1.93/2.00 %MaxLitNum:10 % 1.93/2.00 %MaxfuncDepth:1 % 1.93/2.00 %SharedTerms:2 % 1.93/2.00 [49]P1(a1) % 1.93/2.00 [50]~P2(x501) % 1.93/2.00 [51]P17(x511)+P7(x511) % 1.93/2.00 [52]~P4(x521)+P3(x521) % 1.93/2.00 [53]~P5(x531)+P3(x531) % 1.93/2.00 [54]~P1(x541)+P8(x541) % 1.93/2.00 [55]~P5(x551)+~P4(x551) % 1.93/2.00 [56]~P6(x561)+~P4(x561) % 1.93/2.00 [57]~P6(x571)+~P5(x571) % 1.93/2.00 [58]~P17(x581)+~P7(x581) % 1.93/2.00 [60]~P1(x601)+P4(f2(x601)) % 1.93/2.00 [61]~P8(x611)+P5(f9(x611)) % 1.93/2.00 [62]~P8(x621)+P6(f10(x621)) % 1.93/2.00 [63]~P1(x631)+P9(x631,f3(x631)) % 1.93/2.00 [64]~P8(x641)+P11(x641,f14(x641)) % 1.93/2.00 [65]~P8(x651)+P12(x651,f11(x651)) % 1.93/2.00 [66]~P1(x661)+P13(f3(x661),f2(x661)) % 1.93/2.00 [67]~P8(x671)+P14(f14(x671),f9(x671)) % 1.93/2.00 [68]~P8(x681)+P15(f11(x681),f10(x681)) % 1.93/2.00 [69]~P9(x691,x692)+P10(x691,x692) % 1.93/2.00 [70]~P11(x701,x702)+P10(x701,x702) % 1.93/2.00 [71]~P12(x711,x712)+P10(x711,x712) % 1.93/2.00 [72]~P13(x721,x722)+P16(x721,x722) % 1.93/2.00 [73]~P14(x731,x732)+P16(x731,x732) % 1.93/2.00 [74]~P15(x741,x742)+P16(x741,x742) % 1.93/2.00 [59]P5(x591)+~P3(x591)+P4(x591) % 1.93/2.00 [75]~P10(x753,x752)+~P10(x753,x751)+E(x751,x752)+~P8(x753) % 1.93/2.00 [76]E(x761,x762)+~P1(x763)+~P16(f3(x763),x762)+~P16(f3(x763),x761) % 1.93/2.00 [77]E(x771,x772)+~P8(x773)+~P16(f11(x773),x772)+~P16(f11(x773),x771) % 1.93/2.00 [78]E(x781,x782)+~P8(x783)+~P16(f14(x783),x782)+~P16(f14(x783),x781) % 1.93/2.00 [79]~P8(x791)+~P9(x791,x792)+~P13(x792,x793)+P1(x791)+~P4(x793)+P16(x792,f12(x791,x792)) % 1.93/2.00 [80]~P8(x801)+~P9(x801,x802)+~P13(x802,x803)+P1(x801)+~P4(x803)+P16(x802,f13(x801,x802)) % 1.93/2.00 [81]~P8(x811)+~P9(x811,x812)+~P13(x812,x813)+P1(x811)+~P4(x813)+~E(f13(x811,x812),f12(x811,x812)) % 1.93/2.00 [82]~P11(x821,x823)+~P12(x821,x822)+~P14(x823,x824)+~P15(x822,x825)+P8(x821)+~P5(x824)+~P6(x825)+~E(f6(x821),f7(x821))+P16(x822,f15(x821,x822))+P16(x823,f4(x821,x823)) % 1.93/2.00 [83]~P11(x831,x833)+~P12(x831,x832)+~P14(x833,x834)+~P15(x832,x835)+P8(x831)+~P5(x834)+~P6(x835)+~E(f6(x831),f7(x831))+P16(x832,f15(x831,x832))+P16(x833,f8(x831,x833)) % 1.93/2.00 [84]~P11(x841,x843)+~P12(x841,x842)+~P14(x843,x844)+~P15(x842,x845)+P8(x841)+~P5(x844)+~P6(x845)+~E(f6(x841),f7(x841))+P16(x842,f5(x841,x842))+P16(x843,f4(x841,x843)) % 1.93/2.01 [85]~P11(x851,x853)+~P12(x851,x852)+~P14(x853,x854)+~P15(x852,x855)+P8(x851)+~P5(x854)+~P6(x855)+~E(f6(x851),f7(x851))+P16(x852,f5(x851,x852))+P16(x853,f8(x851,x853)) % 1.93/2.01 [86]~P11(x861,x863)+~P12(x861,x862)+~P14(x863,x864)+~P15(x862,x865)+P8(x861)+~P5(x864)+~P6(x865)+~E(f6(x861),f7(x861))+P16(x862,f15(x861,x862))+~E(f8(x861,x863),f4(x861,x863)) % 1.93/2.01 [87]~P11(x871,x873)+~P12(x871,x872)+~P14(x873,x874)+~P15(x872,x875)+P8(x871)+~P5(x874)+~P6(x875)+~E(f6(x871),f7(x871))+P16(x872,f5(x871,x872))+~E(f8(x871,x873),f4(x871,x873)) % 1.93/2.01 [88]~P11(x881,x882)+~P12(x881,x883)+~P14(x882,x884)+~P15(x883,x885)+P8(x881)+~P5(x884)+~P6(x885)+~E(f6(x881),f7(x881))+P16(x882,f4(x881,x882))+~E(f5(x881,x883),f15(x881,x883)) % 1.93/2.01 [89]~P11(x891,x892)+~P12(x891,x893)+~P14(x892,x894)+~P15(x893,x895)+P8(x891)+~P5(x894)+~P6(x895)+~E(f6(x891),f7(x891))+P16(x892,f8(x891,x892))+~E(f5(x891,x893),f15(x891,x893)) % 1.93/2.01 [90]~P11(x901,x903)+~P12(x901,x902)+~P14(x903,x904)+~P15(x902,x905)+P8(x901)+~P5(x904)+~P6(x905)+P10(x901,f7(x901))+P16(x902,f15(x901,x902))+P16(x903,f4(x901,x903)) % 1.93/2.01 [91]~P11(x911,x913)+~P12(x911,x912)+~P14(x913,x914)+~P15(x912,x915)+P8(x911)+~P5(x914)+~P6(x915)+P10(x911,f7(x911))+P16(x912,f15(x911,x912))+P16(x913,f8(x911,x913)) % 1.93/2.01 [92]~P11(x921,x923)+~P12(x921,x922)+~P14(x923,x924)+~P15(x922,x925)+P8(x921)+~P5(x924)+~P6(x925)+P10(x921,f7(x921))+P16(x922,f5(x921,x922))+P16(x923,f4(x921,x923)) % 1.93/2.01 [93]~P11(x931,x933)+~P12(x931,x932)+~P14(x933,x934)+~P15(x932,x935)+P8(x931)+~P5(x934)+~P6(x935)+P10(x931,f7(x931))+P16(x932,f5(x931,x932))+P16(x933,f8(x931,x933)) % 1.93/2.01 [94]~P11(x941,x943)+~P12(x941,x942)+~P14(x943,x944)+~P15(x942,x945)+P8(x941)+~P5(x944)+~P6(x945)+P10(x941,f6(x941))+P16(x942,f15(x941,x942))+P16(x943,f4(x941,x943)) % 1.93/2.01 [95]~P11(x951,x953)+~P12(x951,x952)+~P14(x953,x954)+~P15(x952,x955)+P8(x951)+~P5(x954)+~P6(x955)+P10(x951,f6(x951))+P16(x952,f15(x951,x952))+P16(x953,f8(x951,x953)) % 1.93/2.01 [96]~P11(x961,x963)+~P12(x961,x962)+~P14(x963,x964)+~P15(x962,x965)+P8(x961)+~P5(x964)+~P6(x965)+P10(x961,f6(x961))+P16(x962,f5(x961,x962))+P16(x963,f4(x961,x963)) % 1.93/2.01 [97]~P11(x971,x973)+~P12(x971,x972)+~P14(x973,x974)+~P15(x972,x975)+P8(x971)+~P5(x974)+~P6(x975)+P10(x971,f6(x971))+P16(x972,f5(x971,x972))+P16(x973,f8(x971,x973)) % 1.93/2.01 [98]~P11(x981,x983)+~P12(x981,x982)+~P14(x983,x984)+~P15(x982,x985)+P8(x981)+~P5(x984)+~P6(x985)+~E(f6(x981),f7(x981))+~E(f5(x981,x982),f15(x981,x982))+~E(f8(x981,x983),f4(x981,x983)) % 1.93/2.01 [99]~P11(x991,x993)+~P12(x991,x992)+~P14(x993,x994)+~P15(x992,x995)+P8(x991)+~P5(x994)+~P6(x995)+P10(x991,f7(x991))+P16(x992,f15(x991,x992))+~E(f8(x991,x993),f4(x991,x993)) % 1.93/2.01 [100]~P11(x1001,x1003)+~P12(x1001,x1002)+~P14(x1003,x1004)+~P15(x1002,x1005)+P8(x1001)+~P5(x1004)+~P6(x1005)+P10(x1001,f7(x1001))+P16(x1002,f5(x1001,x1002))+~E(f8(x1001,x1003),f4(x1001,x1003)) % 1.93/2.01 [101]~P11(x1011,x1012)+~P12(x1011,x1013)+~P14(x1012,x1014)+~P15(x1013,x1015)+P8(x1011)+~P5(x1014)+~P6(x1015)+P10(x1011,f7(x1011))+P16(x1012,f4(x1011,x1012))+~E(f5(x1011,x1013),f15(x1011,x1013)) % 1.93/2.01 [102]~P11(x1021,x1022)+~P12(x1021,x1023)+~P14(x1022,x1024)+~P15(x1023,x1025)+P8(x1021)+~P5(x1024)+~P6(x1025)+P10(x1021,f7(x1021))+P16(x1022,f8(x1021,x1022))+~E(f5(x1021,x1023),f15(x1021,x1023)) % 1.93/2.01 [103]~P11(x1031,x1033)+~P12(x1031,x1032)+~P14(x1033,x1034)+~P15(x1032,x1035)+P8(x1031)+~P5(x1034)+~P6(x1035)+P10(x1031,f6(x1031))+P16(x1032,f15(x1031,x1032))+~E(f8(x1031,x1033),f4(x1031,x1033)) % 1.93/2.01 [104]~P11(x1041,x1043)+~P12(x1041,x1042)+~P14(x1043,x1044)+~P15(x1042,x1045)+P8(x1041)+~P5(x1044)+~P6(x1045)+P10(x1041,f6(x1041))+P16(x1042,f5(x1041,x1042))+~E(f8(x1041,x1043),f4(x1041,x1043)) % 1.93/2.01 [105]~P11(x1051,x1052)+~P12(x1051,x1053)+~P14(x1052,x1054)+~P15(x1053,x1055)+P8(x1051)+~P5(x1054)+~P6(x1055)+P10(x1051,f6(x1051))+P16(x1052,f4(x1051,x1052))+~E(f5(x1051,x1053),f15(x1051,x1053)) % 1.93/2.01 [106]~P11(x1061,x1062)+~P12(x1061,x1063)+~P14(x1062,x1064)+~P15(x1063,x1065)+P8(x1061)+~P5(x1064)+~P6(x1065)+P10(x1061,f6(x1061))+P16(x1062,f8(x1061,x1062))+~E(f5(x1061,x1063),f15(x1061,x1063)) % 1.93/2.01 [107]~P11(x1071,x1073)+~P12(x1071,x1072)+~P14(x1073,x1074)+~P15(x1072,x1075)+P8(x1071)+~P5(x1074)+~P6(x1075)+P10(x1071,f7(x1071))+~E(f5(x1071,x1072),f15(x1071,x1072))+~E(f8(x1071,x1073),f4(x1071,x1073)) % 1.93/2.01 [108]~P11(x1081,x1083)+~P12(x1081,x1082)+~P14(x1083,x1084)+~P15(x1082,x1085)+P8(x1081)+~P5(x1084)+~P6(x1085)+P10(x1081,f6(x1081))+~E(f5(x1081,x1082),f15(x1081,x1082))+~E(f8(x1081,x1083),f4(x1081,x1083)) % 1.93/2.01 %EqnAxiom % 1.93/2.01 [1]E(x11,x11) % 1.93/2.01 [2]E(x22,x21)+~E(x21,x22) % 1.93/2.01 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.93/2.01 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 1.93/2.01 [5]~E(x51,x52)+E(f9(x51),f9(x52)) % 1.93/2.01 [6]~E(x61,x62)+E(f10(x61),f10(x62)) % 1.93/2.01 [7]~E(x71,x72)+E(f3(x71),f3(x72)) % 1.93/2.01 [8]~E(x81,x82)+E(f14(x81),f14(x82)) % 1.93/2.01 [9]~E(x91,x92)+E(f11(x91),f11(x92)) % 1.93/2.01 [10]~E(x101,x102)+E(f5(x101,x103),f5(x102,x103)) % 1.93/2.01 [11]~E(x111,x112)+E(f5(x113,x111),f5(x113,x112)) % 1.93/2.01 [12]~E(x121,x122)+E(f4(x121,x123),f4(x122,x123)) % 1.93/2.01 [13]~E(x131,x132)+E(f4(x133,x131),f4(x133,x132)) % 1.93/2.01 [14]~E(x141,x142)+E(f8(x141,x143),f8(x142,x143)) % 1.93/2.01 [15]~E(x151,x152)+E(f8(x153,x151),f8(x153,x152)) % 1.93/2.01 [16]~E(x161,x162)+E(f7(x161),f7(x162)) % 1.93/2.01 [17]~E(x171,x172)+E(f6(x171),f6(x172)) % 1.93/2.01 [18]~E(x181,x182)+E(f15(x181,x183),f15(x182,x183)) % 1.93/2.01 [19]~E(x191,x192)+E(f15(x193,x191),f15(x193,x192)) % 1.93/2.01 [20]~E(x201,x202)+E(f12(x201,x203),f12(x202,x203)) % 1.93/2.01 [21]~E(x211,x212)+E(f12(x213,x211),f12(x213,x212)) % 1.93/2.01 [22]~E(x221,x222)+E(f13(x221,x223),f13(x222,x223)) % 1.93/2.01 [23]~E(x231,x232)+E(f13(x233,x231),f13(x233,x232)) % 1.93/2.01 [24]~P1(x241)+P1(x242)+~E(x241,x242) % 1.93/2.01 [25]~P2(x251)+P2(x252)+~E(x251,x252) % 1.93/2.01 [26]~P7(x261)+P7(x262)+~E(x261,x262) % 1.93/2.01 [27]~P17(x271)+P17(x272)+~E(x271,x272) % 1.93/2.01 [28]~P3(x281)+P3(x282)+~E(x281,x282) % 1.93/2.01 [29]~P4(x291)+P4(x292)+~E(x291,x292) % 1.93/2.01 [30]P12(x302,x303)+~E(x301,x302)+~P12(x301,x303) % 1.93/2.01 [31]P12(x313,x312)+~E(x311,x312)+~P12(x313,x311) % 1.93/2.01 [32]~P5(x321)+P5(x322)+~E(x321,x322) % 1.93/2.01 [33]~P8(x331)+P8(x332)+~E(x331,x332) % 1.93/2.01 [34]P15(x342,x343)+~E(x341,x342)+~P15(x341,x343) % 1.93/2.01 [35]P15(x353,x352)+~E(x351,x352)+~P15(x353,x351) % 1.93/2.01 [36]~P6(x361)+P6(x362)+~E(x361,x362) % 1.93/2.01 [37]P16(x372,x373)+~E(x371,x372)+~P16(x371,x373) % 1.93/2.01 [38]P16(x383,x382)+~E(x381,x382)+~P16(x383,x381) % 1.93/2.01 [39]P11(x392,x393)+~E(x391,x392)+~P11(x391,x393) % 1.93/2.01 [40]P11(x403,x402)+~E(x401,x402)+~P11(x403,x401) % 1.93/2.01 [41]P14(x412,x413)+~E(x411,x412)+~P14(x411,x413) % 1.93/2.01 [42]P14(x423,x422)+~E(x421,x422)+~P14(x423,x421) % 1.93/2.01 [43]P10(x432,x433)+~E(x431,x432)+~P10(x431,x433) % 1.93/2.01 [44]P10(x443,x442)+~E(x441,x442)+~P10(x443,x441) % 1.93/2.01 [45]P13(x452,x453)+~E(x451,x452)+~P13(x451,x453) % 1.93/2.01 [46]P13(x463,x462)+~E(x461,x462)+~P13(x463,x461) % 1.93/2.01 [47]P9(x472,x473)+~E(x471,x472)+~P9(x471,x473) % 1.93/2.01 [48]P9(x483,x482)+~E(x481,x482)+~P9(x483,x481) % 1.93/2.01 % 1.93/2.01 %------------------------------------------- % 1.93/2.01 cnf(113,plain, % 1.93/2.01 (P5(f9(a1))), % 1.93/2.01 inference(scs_inference,[],[49,54,61])). % 1.93/2.01 cnf(116,plain, % 1.93/2.01 (~P5(f2(a1))), % 1.93/2.01 inference(scs_inference,[],[49,55,60])). % 1.93/2.01 cnf(121,plain, % 1.93/2.01 (~E(a1,x1211)+P9(x1211,f3(x1211))), % 1.93/2.01 inference(scs_inference,[],[49,63,24])). % 1.93/2.01 cnf(122,plain, % 1.93/2.01 (P9(a1,f3(a1))), % 1.93/2.01 inference(equality_inference,[],[121])). % 1.93/2.01 cnf(127,plain, % 1.93/2.01 (P11(a1,f14(a1))), % 1.93/2.01 inference(scs_inference,[],[49,64,54])). % 1.93/2.01 cnf(132,plain, % 1.93/2.01 (P12(a1,f11(a1))), % 1.93/2.01 inference(scs_inference,[],[49,65,54])). % 1.93/2.01 cnf(137,plain, % 1.93/2.01 (P10(x1371,f3(a1))+~E(a1,x1371)), % 1.93/2.01 inference(scs_inference,[],[122,69,43])). % 1.93/2.01 cnf(138,plain, % 1.93/2.01 (P10(a1,f3(a1))), % 1.93/2.01 inference(equality_inference,[],[137])). % 1.93/2.01 cnf(142,plain, % 1.93/2.01 (P10(a1,x1421)+~E(f14(a1),x1421)), % 1.93/2.01 inference(scs_inference,[],[127,70,44])). % 1.93/2.01 cnf(143,plain, % 1.93/2.01 (P10(a1,f14(a1))), % 1.93/2.01 inference(equality_inference,[],[142])). % 1.93/2.01 cnf(147,plain, % 1.93/2.01 (P10(x1471,f11(a1))+~E(a1,x1471)), % 1.93/2.01 inference(scs_inference,[],[132,71,43])). % 1.93/2.01 cnf(148,plain, % 1.93/2.01 (P10(a1,f11(a1))), % 1.93/2.01 inference(equality_inference,[],[147])). % 1.93/2.01 cnf(158,plain, % 1.93/2.01 (~E(a1,x1581)+P13(f3(x1581),f2(x1581))), % 1.93/2.01 inference(scs_inference,[],[49,66,24])). % 1.93/2.01 cnf(159,plain, % 1.93/2.01 (P13(f3(a1),f2(a1))), % 1.93/2.01 inference(equality_inference,[],[158])). % 1.93/2.01 cnf(160,plain, % 1.93/2.01 (P13(x1601,f2(a1))+~E(f3(a1),x1601)), % 1.93/2.01 inference(scs_inference,[],[159,45])). % 1.93/2.01 cnf(164,plain, % 1.93/2.01 (P14(f14(a1),f9(a1))), % 1.93/2.01 inference(scs_inference,[],[49,67,54])). % 1.93/2.01 cnf(165,plain, % 1.93/2.01 (P14(x1651,f9(a1))+~E(f14(a1),x1651)), % 1.93/2.01 inference(scs_inference,[],[164,41])). % 1.93/2.01 cnf(697,plain, % 1.93/2.01 (~P8(x6971)+~P16(f11(x6971),f2(a1))+~P16(f11(x6971),f9(a1))), % 1.93/2.01 inference(scs_inference,[],[113,116,77,32])). % 1.93/2.01 cnf(713,plain, % 1.93/2.01 (~P16(f11(a1),f2(a1))+~P16(f11(a1),f9(a1))), % 1.93/2.01 inference(scs_inference,[],[49,697,54])). % 1.93/2.01 cnf(729,plain, % 1.93/2.01 (~P13(f11(a1),f2(a1))+~P16(f11(a1),f9(a1))), % 1.93/2.01 inference(scs_inference,[],[713,72])). % 1.93/2.01 cnf(745,plain, % 1.93/2.01 (~E(f3(a1),f11(a1))+~P16(f11(a1),f9(a1))), % 1.93/2.01 inference(scs_inference,[],[729,160])). % 1.93/2.01 cnf(761,plain, % 1.93/2.01 (~E(f11(a1),f3(a1))+~P16(f11(a1),f9(a1))), % 1.93/2.01 inference(scs_inference,[],[745,2])). % 1.93/2.01 cnf(777,plain, % 1.93/2.01 (~P8(a1)+~P16(f11(a1),f9(a1))), % 1.93/2.01 inference(scs_inference,[],[138,148,761,75])). % 1.93/2.01 cnf(793,plain, % 1.93/2.01 (~P14(f11(a1),f9(a1))+~P8(a1)), % 1.93/2.01 inference(scs_inference,[],[777,73])). % 1.93/2.01 cnf(809,plain, % 1.93/2.01 (~E(f14(a1),f11(a1))+~P8(a1)), % 1.93/2.01 inference(scs_inference,[],[793,165])). % 1.93/2.01 cnf(825,plain, % 1.93/2.01 (~P8(a1)), % 1.93/2.01 inference(scs_inference,[],[148,143,809,75])). % 1.93/2.01 cnf(826,plain, % 1.93/2.01 ($false), % 1.93/2.01 inference(scs_inference,[],[825,49,54]), % 1.93/2.01 ['proof']). % 1.93/2.01 % SZS output end Proof % 1.93/2.01 % Total time :1.340000s %------------------------------------------------------------------------------