%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS108+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 : n016.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:31 EDT 2024 % Result : Unsatisfiable 0.90s 0.97s % Output : CNFRefutation 0.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.10 % Problem : KRS108+1 : TPTP v8.2.0. Released v3.1.0. % 0.05/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n016.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Wed Jun 19 13:29:08 EDT 2024 % 0.10/0.31 % CPUTime : % 0.16/0.51 start to proof:theBenchmark % 0.87/0.96 %------------------------------------------- % 0.87/0.96 % File :CSE---1.7 % 0.87/0.96 % Problem :theBenchmark % 0.87/0.96 % Transform :cnf % 0.87/0.96 % Format :tptp:raw % 0.87/0.96 % Command :java -jar mcs_scs.jar %d %s % 0.87/0.96 % 0.87/0.96 % Result :Theorem 0.420000s % 0.87/0.96 % Output :CNFRefutation 0.420000s % 0.87/0.96 %------------------------------------------- % 0.87/0.97 %------------------------------------------------------------------------------ % 0.87/0.97 % File : KRS108+1 : TPTP v8.2.0. Released v3.1.0. % 0.87/0.97 % Domain : Knowledge Representation (Semantic Web) % 0.87/0.97 % Problem : DL Test: t1.3 % 0.87/0.97 % Version : Especial. % 0.87/0.97 % English : % 0.87/0.97 % 0.87/0.97 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 0.87/0.97 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 0.87/0.97 % Source : [Bec03] % 0.87/0.97 % Names : inconsistent_description-logic-Manifest608 [Bec03] % 0.87/0.97 % 0.87/0.97 % Status : Unsatisfiable % 0.87/0.97 % Rating : 0.00 v3.1.0 % 0.87/0.97 % Syntax : Number of formulae : 66 ( 1 unt; 0 def) % 0.87/0.97 % Number of atoms : 182 ( 40 equ) % 0.87/0.97 % Maximal formula atoms : 6 ( 2 avg) % 0.87/0.97 % Number of connectives : 125 ( 9 ~; 0 |; 51 &) % 0.87/0.97 % ( 21 <=>; 44 =>; 0 <=; 0 <~>) % 0.87/0.97 % Maximal formula depth : 8 ( 5 avg) % 0.87/0.97 % Maximal term depth : 1 ( 1 avg) % 0.87/0.97 % Number of predicates : 31 ( 30 usr; 0 prp; 1-2 aty) % 0.87/0.97 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 0.87/0.97 % Number of variables : 141 ( 125 !; 16 ?) % 0.87/0.97 % SPC : FOF_UNS_RFO_SEQ % 0.87/0.97 % 0.87/0.97 % Comments : Sean Bechhofer says there are some errors in the encoding of % 0.87/0.97 % datatypes, so this problem may not be perfect. At least it's % 0.87/0.97 % still representative of the type of reasoning required for OWL. % 0.87/0.97 %------------------------------------------------------------------------------ % 0.87/0.97 fof(cUnsatisfiable_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cUnsatisfiable(A) ) % 0.87/0.97 => cUnsatisfiable(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ca_Ax14_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ca_Ax14(A) ) % 0.87/0.97 => ca_Ax14(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ca_Cx1_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ca_Cx1(A) ) % 0.87/0.97 => ca_Cx1(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ca_Cx1xcomp_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ca_Cx1xcomp(A) ) % 0.87/0.97 => ca_Cx1xcomp(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ca_Cx2_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ca_Cx2(A) ) % 0.87/0.97 => ca_Cx2(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ca_Cx2xcomp_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ca_Cx2xcomp(A) ) % 0.87/0.97 => ca_Cx2xcomp(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ca_Cx3_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ca_Cx3(A) ) % 0.87/0.97 => ca_Cx3(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ca_Cx3xcomp_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ca_Cx3xcomp(A) ) % 0.87/0.97 => ca_Cx3xcomp(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(cowlNothing_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cowlNothing(A) ) % 0.87/0.97 => cowlNothing(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(cowlThing_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cowlThing(A) ) % 0.87/0.97 => cowlThing(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(cp1_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cp1(A) ) % 0.87/0.97 => cp1(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(cp2_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cp2(A) ) % 0.87/0.97 => cp2(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(cp2xcomp_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cp2xcomp(A) ) % 0.87/0.97 => cp2xcomp(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(cp3_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cp3(A) ) % 0.87/0.97 => cp3(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(cp3xcomp_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cp3xcomp(A) ) % 0.87/0.97 => cp3xcomp(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(cp4_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cp4(A) ) % 0.87/0.97 => cp4(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(cp4xcomp_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cp4xcomp(A) ) % 0.87/0.97 => cp4xcomp(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(cp5_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cp5(A) ) % 0.87/0.97 => cp5(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(cp5xcomp_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & cp5xcomp(A) ) % 0.87/0.97 => cp5xcomp(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px1_substitution_1,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px1(A,C) ) % 0.87/0.97 => ra_Px1(B,C) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px1_substitution_2,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px1(C,A) ) % 0.87/0.97 => ra_Px1(C,B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px2_substitution_1,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px2(A,C) ) % 0.87/0.97 => ra_Px2(B,C) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px2_substitution_2,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px2(C,A) ) % 0.87/0.97 => ra_Px2(C,B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px3_substitution_1,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px3(A,C) ) % 0.87/0.97 => ra_Px3(B,C) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px3_substitution_2,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px3(C,A) ) % 0.87/0.97 => ra_Px3(C,B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px4_substitution_1,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px4(A,C) ) % 0.87/0.97 => ra_Px4(B,C) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px4_substitution_2,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px4(C,A) ) % 0.87/0.97 => ra_Px4(C,B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px5_substitution_1,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px5(A,C) ) % 0.87/0.97 => ra_Px5(B,C) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px5_substitution_2,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px5(C,A) ) % 0.87/0.97 => ra_Px5(C,B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px6_substitution_1,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px6(A,C) ) % 0.87/0.97 => ra_Px6(B,C) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px6_substitution_2,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px6(C,A) ) % 0.87/0.97 => ra_Px6(C,B) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px7_substitution_1,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px7(A,C) ) % 0.87/0.97 => ra_Px7(B,C) ) ). % 0.87/0.97 % 0.87/0.97 fof(ra_Px7_substitution_2,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & ra_Px7(C,A) ) % 0.87/0.97 => ra_Px7(C,B) ) ). % 0.87/0.97 % 0.87/0.97 fof(rinvR_substitution_1,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & rinvR(A,C) ) % 0.87/0.97 => rinvR(B,C) ) ). % 0.87/0.97 % 0.87/0.97 fof(rinvR_substitution_2,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & rinvR(C,A) ) % 0.87/0.97 => rinvR(C,B) ) ). % 0.87/0.97 % 0.87/0.97 fof(rr_substitution_1,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & rr(A,C) ) % 0.87/0.97 => rr(B,C) ) ). % 0.87/0.97 % 0.87/0.97 fof(rr_substitution_2,axiom, % 0.87/0.97 ! [A,B,C] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & rr(C,A) ) % 0.87/0.97 => rr(C,B) ) ). % 0.87/0.97 % 0.87/0.97 fof(xsd_integer_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & xsd_integer(A) ) % 0.87/0.97 => xsd_integer(B) ) ). % 0.87/0.97 % 0.87/0.97 fof(xsd_string_substitution_1,axiom, % 0.87/0.97 ! [A,B] : % 0.87/0.97 ( ( A = B % 0.87/0.97 & xsd_string(A) ) % 0.87/0.97 => xsd_string(B) ) ). % 0.87/0.97 % 0.87/0.97 %----Thing and Nothing % 0.87/0.97 fof(axiom_0,axiom, % 0.87/0.97 ! [X] : % 0.87/0.97 ( cowlThing(X) % 0.87/0.97 & ~ cowlNothing(X) ) ). % 0.87/0.97 % 0.87/0.97 %----String and Integer disjoint % 0.87/0.97 fof(axiom_1,axiom, % 0.87/0.97 ! [X] : % 0.87/0.97 ( xsd_string(X) % 0.87/0.97 <=> ~ xsd_integer(X) ) ). % 0.87/0.97 % 0.87/0.97 %----Equality cUnsatisfiable % 0.87/0.97 fof(axiom_2,axiom, % 0.87/0.97 ! [X] : % 0.87/0.97 ( cUnsatisfiable(X) % 0.87/0.97 <=> ( ? [Y] : % 0.87/0.97 ( rinvR(X,Y) % 0.87/0.97 & ca_Ax14(Y) ) % 0.87/0.97 & cp2(X) ) ) ). % 0.87/0.97 % 0.87/0.97 %----Super cp1 % 0.87/0.97 fof(axiom_3,axiom, % 0.87/0.97 ! [X] : % 0.87/0.97 ( cp1(X) % 0.87/0.97 => ca_Cx1(X) ) ). % 0.87/0.97 % 0.87/0.97 %----Equality cp2 % 0.87/0.97 fof(axiom_4,axiom, % 0.87/0.97 ! [X] : % 0.87/0.97 ( cp2(X) % 0.87/0.97 <=> ? [Y0] : ra_Px5(X,Y0) ) ). % 0.87/0.97 % 0.87/0.97 %----Super cp2 % 0.87/0.97 fof(axiom_5,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( cp2(X) % 0.90/0.97 => ca_Cx2(X) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality cp2xcomp % 0.90/0.97 fof(axiom_6,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( cp2xcomp(X) % 0.90/0.97 <=> ~ ? [Y] : ra_Px5(X,Y) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality cp3 % 0.90/0.97 fof(axiom_7,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( cp3(X) % 0.90/0.97 <=> ? [Y0] : ra_Px6(X,Y0) ) ). % 0.90/0.97 % 0.90/0.97 %----Super cp3 % 0.90/0.97 fof(axiom_8,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( cp3(X) % 0.90/0.97 => ca_Cx3(X) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality cp3xcomp % 0.90/0.97 fof(axiom_9,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( cp3xcomp(X) % 0.90/0.97 <=> ~ ? [Y] : ra_Px6(X,Y) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality cp4 % 0.90/0.97 fof(axiom_10,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( cp4(X) % 0.90/0.97 <=> ~ ? [Y] : ra_Px7(X,Y) ) ). % 0.90/0.97 % 0.90/0.97 %----Super cp4 % 0.90/0.97 fof(axiom_11,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( cp4(X) % 0.90/0.97 => cp5xcomp(X) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality cp4xcomp % 0.90/0.97 fof(axiom_12,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( cp4xcomp(X) % 0.90/0.97 <=> ? [Y0] : ra_Px7(X,Y0) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality cp5 % 0.90/0.97 fof(axiom_13,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( cp5(X) % 0.90/0.97 <=> ~ ? [Y] : ra_Px4(X,Y) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality cp5xcomp % 0.90/0.97 fof(axiom_14,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( cp5xcomp(X) % 0.90/0.97 <=> ? [Y0] : ra_Px4(X,Y0) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality ca_Ax14 % 0.90/0.97 fof(axiom_15,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( ca_Ax14(X) % 0.90/0.97 <=> ( ? [Y] : % 0.90/0.97 ( rr(X,Y) % 0.90/0.97 & cp1(Y) ) % 0.90/0.97 & ! [Y0,Y1] : % 0.90/0.97 ( ( rr(X,Y0) % 0.90/0.97 & rr(X,Y1) ) % 0.90/0.97 => Y0 = Y1 ) ) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality ca_Cx1 % 0.90/0.97 fof(axiom_16,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( ca_Cx1(X) % 0.90/0.97 <=> ( cp2xcomp(X) % 0.90/0.97 & cp5xcomp(X) % 0.90/0.97 & cp3xcomp(X) % 0.90/0.97 & cp4xcomp(X) ) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality ca_Cx1 % 0.90/0.97 fof(axiom_17,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( ca_Cx1(X) % 0.90/0.97 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality ca_Cx1xcomp % 0.90/0.97 fof(axiom_18,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( ca_Cx1xcomp(X) % 0.90/0.97 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality ca_Cx2 % 0.90/0.97 fof(axiom_19,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( ca_Cx2(X) % 0.90/0.97 <=> ( cp5xcomp(X) % 0.90/0.97 & cp3xcomp(X) % 0.90/0.97 & cp4xcomp(X) ) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality ca_Cx2 % 0.90/0.97 fof(axiom_20,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( ca_Cx2(X) % 0.90/0.97 <=> ~ ? [Y] : ra_Px2(X,Y) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality ca_Cx2xcomp % 0.90/0.97 fof(axiom_21,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( ca_Cx2xcomp(X) % 0.90/0.97 <=> ? [Y0] : ra_Px2(X,Y0) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality ca_Cx3 % 0.90/0.97 fof(axiom_22,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( ca_Cx3(X) % 0.90/0.97 <=> ~ ? [Y] : ra_Px3(X,Y) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality ca_Cx3 % 0.90/0.97 fof(axiom_23,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( ca_Cx3(X) % 0.90/0.97 <=> ( cp5xcomp(X) % 0.90/0.97 & cp4xcomp(X) ) ) ). % 0.90/0.97 % 0.90/0.97 %----Equality ca_Cx3xcomp % 0.90/0.97 fof(axiom_24,axiom, % 0.90/0.97 ! [X] : % 0.90/0.97 ( ca_Cx3xcomp(X) % 0.90/0.97 <=> ? [Y0] : ra_Px3(X,Y0) ) ). % 0.90/0.97 % 0.90/0.97 %----Inverse: rinvR % 0.90/0.97 fof(axiom_25,axiom, % 0.90/0.97 ! [X,Y] : % 0.90/0.97 ( rinvR(X,Y) % 0.90/0.97 <=> rr(Y,X) ) ). % 0.90/0.97 % 0.90/0.97 %----i2003_11_14_17_21_04740 % 0.90/0.97 fof(axiom_26,axiom, % 0.90/0.97 cUnsatisfiable(i2003_11_14_17_21_04740) ). % 0.90/0.97 % 0.90/0.97 %------------------------------------------------------------------------------ % 0.90/0.97 %------------------------------------------- % 0.90/0.97 % Proof found % 0.90/0.97 % SZS status Theorem for theBenchmark % 0.90/0.97 % SZS output start Proof % 0.90/0.98 %ClaNum:119(EqnAxiom:59) % 0.90/0.98 %VarNum:177(SingletonVarNum:81) % 0.90/0.98 %MaxLitNum:5 % 0.90/0.98 %MaxfuncDepth:1 % 0.90/0.98 %SharedTerms:2 % 0.90/0.98 [60]P1(a1) % 0.90/0.98 [61]~P2(x611) % 0.90/0.98 [62]P29(x621)+P10(x621) % 0.90/0.98 [63]~P11(x631)+P3(x631) % 0.90/0.98 [64]~P12(x641)+P5(x641) % 0.90/0.98 [65]~P13(x651)+P7(x651) % 0.90/0.98 [66]~P1(x661)+P12(x661) % 0.90/0.98 [67]~P3(x671)+P14(x671) % 0.90/0.98 [68]~P3(x681)+P15(x681) % 0.90/0.98 [69]~P5(x691)+P15(x691) % 0.90/0.98 [70]~P3(x701)+P16(x701) % 0.90/0.98 [71]~P5(x711)+P16(x711) % 0.90/0.98 [72]~P7(x721)+P16(x721) % 0.90/0.98 [73]~P3(x731)+P18(x731) % 0.90/0.98 [74]~P5(x741)+P18(x741) % 0.90/0.98 [75]~P7(x751)+P18(x751) % 0.90/0.98 [76]~P17(x761)+P18(x761) % 0.90/0.98 [77]~P29(x771)+~P10(x771) % 0.90/0.98 [78]~P1(x781)+P4(f2(x781)) % 0.90/0.98 [79]~P4(x791)+P11(f3(x791)) % 0.90/0.98 [81]P6(x811)+P20(x811,f4(x811)) % 0.90/0.98 [82]P5(x821)+P21(x821,f8(x821)) % 0.90/0.98 [83]P7(x831)+P22(x831,f9(x831)) % 0.90/0.98 [84]P14(x841)+P23(x841,f12(x841)) % 0.90/0.98 [85]P15(x851)+P25(x851,f14(x851)) % 0.90/0.98 [86]P17(x861)+P26(x861,f16(x861)) % 0.90/0.98 [87]P19(x871)+P24(x871,f17(x871)) % 0.90/0.98 [96]~P3(x961)+P20(x961,f5(x961)) % 0.90/0.98 [97]~P8(x971)+P21(x971,f10(x971)) % 0.90/0.98 [98]~P9(x981)+P22(x981,f11(x981)) % 0.90/0.98 [99]~P18(x991)+P24(x991,f19(x991)) % 0.90/0.98 [100]~P12(x1001)+P23(x1001,f13(x1001)) % 0.90/0.98 [101]~P13(x1011)+P25(x1011,f15(x1011)) % 0.90/0.98 [102]~P16(x1021)+P26(x1021,f18(x1021)) % 0.90/0.98 [103]~P1(x1031)+P27(x1031,f2(x1031)) % 0.90/0.98 [104]~P4(x1041)+P28(x1041,f3(x1041)) % 0.90/0.98 [89]P3(x891)+~P20(x891,x892) % 0.90/0.98 [90]P8(x901)+~P21(x901,x902) % 0.90/0.98 [91]P9(x911)+~P22(x911,x912) % 0.90/0.98 [92]P12(x921)+~P23(x921,x922) % 0.90/0.98 [93]P13(x931)+~P25(x931,x932) % 0.90/0.98 [94]P16(x941)+~P26(x941,x942) % 0.90/0.98 [95]P18(x951)+~P24(x951,x952) % 0.90/0.98 [105]~P6(x1051)+~P20(x1051,x1052) % 0.90/0.98 [106]~P5(x1061)+~P21(x1061,x1062) % 0.90/0.98 [107]~P7(x1071)+~P22(x1071,x1072) % 0.90/0.98 [108]~P14(x1081)+~P23(x1081,x1082) % 0.90/0.98 [109]~P15(x1091)+~P25(x1091,x1092) % 0.90/0.98 [110]~P17(x1101)+~P26(x1101,x1102) % 0.90/0.98 [111]~P19(x1111)+~P24(x1111,x1112) % 0.90/0.98 [113]~P28(x1132,x1131)+P27(x1131,x1132) % 0.90/0.98 [114]~P27(x1142,x1141)+P28(x1141,x1142) % 0.90/0.98 [80]~P16(x801)+~P18(x801)+P7(x801) % 0.90/0.98 [88]~P15(x881)+~P16(x881)+~P18(x881)+P5(x881) % 0.90/0.98 [115]~P12(x1151)+~P27(x1151,x1152)+P1(x1151)+~P4(x1152) % 0.90/0.98 [116]~P28(x1161,x1162)+P4(x1161)+~P11(x1162)+~E(f6(x1161),f7(x1161)) % 0.90/0.98 [118]~P28(x1181,x1182)+P4(x1181)+~P11(x1182)+P28(x1181,f7(x1181)) % 0.90/0.98 [119]~P28(x1191,x1192)+P4(x1191)+~P11(x1192)+P28(x1191,f6(x1191)) % 0.90/0.98 [117]~P28(x1173,x1172)+~P28(x1173,x1171)+E(x1171,x1172)+~P4(x1173) % 0.90/0.98 [112]~P14(x1121)+~P15(x1121)+~P16(x1121)+~P18(x1121)+P3(x1121) % 0.90/0.98 %EqnAxiom % 0.90/0.98 [1]E(x11,x11) % 0.90/0.98 [2]E(x22,x21)+~E(x21,x22) % 0.90/0.98 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.90/0.98 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.90/0.98 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 0.90/0.98 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 0.90/0.98 [7]~E(x71,x72)+E(f8(x71),f8(x72)) % 0.90/0.98 [8]~E(x81,x82)+E(f9(x81),f9(x82)) % 0.90/0.98 [9]~E(x91,x92)+E(f12(x91),f12(x92)) % 0.90/0.98 [10]~E(x101,x102)+E(f14(x101),f14(x102)) % 0.90/0.98 [11]~E(x111,x112)+E(f16(x111),f16(x112)) % 0.90/0.98 [12]~E(x121,x122)+E(f17(x121),f17(x122)) % 0.90/0.98 [13]~E(x131,x132)+E(f5(x131),f5(x132)) % 0.90/0.98 [14]~E(x141,x142)+E(f10(x141),f10(x142)) % 0.90/0.98 [15]~E(x151,x152)+E(f11(x151),f11(x152)) % 0.90/0.98 [16]~E(x161,x162)+E(f19(x161),f19(x162)) % 0.90/0.98 [17]~E(x171,x172)+E(f13(x171),f13(x172)) % 0.90/0.98 [18]~E(x181,x182)+E(f15(x181),f15(x182)) % 0.90/0.98 [19]~E(x191,x192)+E(f18(x191),f18(x192)) % 0.90/0.98 [20]~E(x201,x202)+E(f6(x201),f6(x202)) % 0.90/0.98 [21]~E(x211,x212)+E(f7(x211),f7(x212)) % 0.90/0.98 [22]~P1(x221)+P1(x222)+~E(x221,x222) % 0.90/0.98 [23]~P2(x231)+P2(x232)+~E(x231,x232) % 0.90/0.98 [24]~P10(x241)+P10(x242)+~E(x241,x242) % 0.90/0.98 [25]~P29(x251)+P29(x252)+~E(x251,x252) % 0.90/0.98 [26]~P3(x261)+P3(x262)+~E(x261,x262) % 0.90/0.98 [27]~P11(x271)+P11(x272)+~E(x271,x272) % 0.90/0.98 [28]~P5(x281)+P5(x282)+~E(x281,x282) % 0.90/0.98 [29]~P12(x291)+P12(x292)+~E(x291,x292) % 0.90/0.98 [30]~P7(x301)+P7(x302)+~E(x301,x302) % 0.90/0.98 [31]~P13(x311)+P13(x312)+~E(x311,x312) % 0.90/0.98 [32]~P16(x321)+P16(x322)+~E(x321,x322) % 0.90/0.98 [33]P28(x332,x333)+~E(x331,x332)+~P28(x331,x333) % 0.90/0.98 [34]P28(x343,x342)+~E(x341,x342)+~P28(x343,x341) % 0.90/0.98 [35]~P14(x351)+P14(x352)+~E(x351,x352) % 0.90/0.98 [36]~P4(x361)+P4(x362)+~E(x361,x362) % 0.90/0.98 [37]~P15(x371)+P15(x372)+~E(x371,x372) % 0.90/0.98 [38]~P9(x381)+P9(x382)+~E(x381,x382) % 0.90/0.98 [39]~P18(x391)+P18(x392)+~E(x391,x392) % 0.90/0.98 [40]P22(x402,x403)+~E(x401,x402)+~P22(x401,x403) % 0.90/0.98 [41]P22(x413,x412)+~E(x411,x412)+~P22(x413,x411) % 0.90/0.98 [42]P23(x422,x423)+~E(x421,x422)+~P23(x421,x423) % 0.90/0.98 [43]P23(x433,x432)+~E(x431,x432)+~P23(x433,x431) % 0.90/0.98 [44]P27(x442,x443)+~E(x441,x442)+~P27(x441,x443) % 0.90/0.98 [45]P27(x453,x452)+~E(x451,x452)+~P27(x453,x451) % 0.90/0.98 [46]P24(x462,x463)+~E(x461,x462)+~P24(x461,x463) % 0.90/0.98 [47]P24(x473,x472)+~E(x471,x472)+~P24(x473,x471) % 0.90/0.98 [48]~P17(x481)+P17(x482)+~E(x481,x482) % 0.90/0.98 [49]P25(x492,x493)+~E(x491,x492)+~P25(x491,x493) % 0.90/0.98 [50]P25(x503,x502)+~E(x501,x502)+~P25(x503,x501) % 0.90/0.98 [51]P26(x512,x513)+~E(x511,x512)+~P26(x511,x513) % 0.90/0.98 [52]P26(x523,x522)+~E(x521,x522)+~P26(x523,x521) % 0.90/0.98 [53]P20(x532,x533)+~E(x531,x532)+~P20(x531,x533) % 0.90/0.98 [54]P20(x543,x542)+~E(x541,x542)+~P20(x543,x541) % 0.90/0.98 [55]~P6(x551)+P6(x552)+~E(x551,x552) % 0.90/0.98 [56]P21(x562,x563)+~E(x561,x562)+~P21(x561,x563) % 0.90/0.98 [57]P21(x573,x572)+~E(x571,x572)+~P21(x573,x571) % 0.90/0.98 [58]~P8(x581)+P8(x582)+~E(x581,x582) % 0.90/0.98 [59]~P19(x591)+P19(x592)+~E(x591,x592) % 0.90/0.98 % 0.90/0.98 %------------------------------------------- % 0.90/0.98 cnf(121,plain, % 0.90/0.98 (P14(x1211)+~P11(x1211)), % 0.90/0.98 inference(scs_inference,[],[63,67])). % 0.90/0.98 cnf(124,plain, % 0.90/0.98 (P23(a1,f13(a1))), % 0.90/0.98 inference(scs_inference,[],[60,66,100])). % 0.90/0.98 cnf(136,plain, % 0.90/0.98 (P14(f3(x1361))+~P4(x1361)), % 0.90/0.98 inference(scs_inference,[],[121,79])). % 0.90/0.98 cnf(159,plain, % 0.90/0.98 (~E(a1,x1591)+P4(f2(x1591))), % 0.90/0.98 inference(scs_inference,[],[60,78,22])). % 0.90/0.98 cnf(160,plain, % 0.90/0.98 (P4(f2(a1))), % 0.90/0.98 inference(equality_inference,[],[159])). % 0.90/0.98 cnf(166,plain, % 0.90/0.98 (~P28(f2(a1),f3(f2(a1)))+~P28(f2(a1),a1)), % 0.90/0.98 inference(scs_inference,[],[124,160,136,108,42,117])). % 0.90/0.98 cnf(461,plain, % 0.90/0.98 (~E(a1,x4611)+P27(x4611,f2(x4611))), % 0.90/0.98 inference(scs_inference,[],[60,103,22])). % 0.90/0.98 cnf(462,plain, % 0.90/0.98 (P27(a1,f2(a1))), % 0.90/0.98 inference(equality_inference,[],[461])). % 0.90/0.98 cnf(536,plain, % 0.90/0.98 (~P28(f2(a1),a1)), % 0.90/0.98 inference(scs_inference,[],[160,166,104])). % 0.90/0.98 cnf(537,plain, % 0.90/0.98 ($false), % 0.90/0.98 inference(scs_inference,[],[462,536,114]), % 0.90/0.98 ['proof']). % 0.90/0.98 % SZS output end Proof % 0.90/0.98 % Total time :0.420000s %------------------------------------------------------------------------------