%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS104+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n010.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:30 EDT 2024 % Result : Unsatisfiable 58.55s 58.69s % Output : CNFRefutation 58.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS104+1 : TPTP v8.2.0. Released v3.1.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n010.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Wed Jun 19 12:40:08 EDT 2024 % 0.11/0.33 % CPUTime : % 0.49/0.56 start to proof:theBenchmark % 58.55/58.67 %------------------------------------------- % 58.55/58.67 % File :CSE---1.7 % 58.55/58.67 % Problem :theBenchmark % 58.55/58.67 % Transform :cnf % 58.55/58.67 % Format :tptp:raw % 58.55/58.67 % Command :java -jar mcs_scs.jar %d %s % 58.55/58.67 % 58.55/58.67 % Result :Theorem 58.000000s % 58.55/58.67 % Output :CNFRefutation 58.000000s % 58.55/58.67 %------------------------------------------- % 58.55/58.68 %------------------------------------------------------------------------------ % 58.55/58.68 % File : KRS104+1 : TPTP v8.2.0. Released v3.1.0. % 58.55/58.68 % Domain : Knowledge Representation (Semantic Web) % 58.55/58.68 % Problem : DL Test: fact1.1 % 58.55/58.68 % Version : Especial. % 58.55/58.68 % English : If a, b and c are disjoint, then: % 58.55/58.68 % (a and b) or (b and c) or (c and a) % 58.55/58.68 % is unsatisfiable. % 58.55/58.68 % 58.55/58.68 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 58.55/58.68 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 58.55/58.68 % Source : [Bec03] % 58.55/58.68 % Names : inconsistent_description-logic-Manifest601 [Bec03] % 58.55/58.68 % 58.55/58.68 % Status : Unsatisfiable % 58.55/58.68 % Rating : 0.00 v6.4.0, 0.25 v6.3.0, 0.00 v6.2.0, 0.25 v6.1.0, 0.00 v3.1.0 % 58.55/58.68 % Syntax : Number of formulae : 24 ( 1 unt; 0 def) % 58.55/58.68 % Number of atoms : 53 ( 0 equ) % 58.55/58.68 % Maximal formula atoms : 4 ( 2 avg) % 58.55/58.68 % Number of connectives : 38 ( 9 ~; 0 |; 7 &) % 58.55/58.68 % ( 20 <=>; 2 =>; 0 <=; 0 <~>) % 58.55/58.68 % Maximal formula depth : 5 ( 4 avg) % 58.55/58.68 % Maximal term depth : 1 ( 1 avg) % 58.55/58.68 % Number of predicates : 26 ( 26 usr; 0 prp; 1-2 aty) % 58.55/58.68 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 58.55/58.68 % Number of variables : 37 ( 23 !; 14 ?) % 58.55/58.68 % SPC : FOF_UNS_RFO_NEQ % 58.55/58.68 % 58.55/58.68 % Comments : Sean Bechhofer says there are some errors in the encoding of % 58.55/58.68 % datatypes, so this problem may not be perfect. At least it's % 58.55/58.68 % still representative of the type of reasoning required for OWL. % 58.55/58.68 %------------------------------------------------------------------------------ % 58.55/58.68 %----Thing and Nothing % 58.55/58.68 fof(axiom_0,axiom, % 58.55/58.68 ! [X] : % 58.55/58.68 ( cowlThing(X) % 58.55/58.68 & ~ cowlNothing(X) ) ). % 58.55/58.69 % 58.55/58.69 %----String and Integer disjoint % 58.55/58.69 fof(axiom_1,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( xsd_string(X) % 58.55/58.69 <=> ~ xsd_integer(X) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality cUnsatisfiable % 58.55/58.69 fof(axiom_2,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( cUnsatisfiable(X) % 58.55/58.69 <=> ~ ? [Y] : ra_Px5(X,Y) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality cUnsatisfiablexcomp % 58.55/58.69 fof(axiom_3,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( cUnsatisfiablexcomp(X) % 58.55/58.69 <=> ( ca_Cx7(X) % 58.55/58.69 & ca_Cx8(X) % 58.55/58.69 & ca_Cx6(X) ) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality cUnsatisfiablexcomp % 58.55/58.69 fof(axiom_4,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( cUnsatisfiablexcomp(X) % 58.55/58.69 <=> ? [Y0] : ra_Px5(X,Y0) ) ). % 58.55/58.69 % 58.55/58.69 %----Super ca % 58.55/58.69 fof(axiom_5,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca(X) % 58.55/58.69 => ca_Cx1(X) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality cb % 58.55/58.69 fof(axiom_6,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( cb(X) % 58.55/58.69 <=> ? [Y0] : ra_Px3(X,Y0) ) ). % 58.55/58.69 % 58.55/58.69 %----Super cb % 58.55/58.69 fof(axiom_7,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( cb(X) % 58.55/58.69 => ccxcomp(X) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality cbxcomp % 58.55/58.69 fof(axiom_8,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( cbxcomp(X) % 58.55/58.69 <=> ~ ? [Y] : ra_Px3(X,Y) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality cc % 58.55/58.69 fof(axiom_9,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( cc(X) % 58.55/58.69 <=> ? [Y0] : ra_Px2(X,Y0) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ccxcomp % 58.55/58.69 fof(axiom_10,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ccxcomp(X) % 58.55/58.69 <=> ~ ? [Y] : ra_Px2(X,Y) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx1 % 58.55/58.69 fof(axiom_11,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx1(X) % 58.55/58.69 <=> ( cbxcomp(X) % 58.55/58.69 & ccxcomp(X) ) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx1 % 58.55/58.69 fof(axiom_12,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx1(X) % 58.55/58.69 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx1xcomp % 58.55/58.69 fof(axiom_13,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx1xcomp(X) % 58.55/58.69 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx6 % 58.55/58.69 fof(axiom_14,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx6(X) % 58.55/58.69 <=> ~ ? [Y] : ra_Px6(X,Y) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx6xcomp % 58.55/58.69 fof(axiom_15,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx6xcomp(X) % 58.55/58.69 <=> ( ca(X) % 58.55/58.69 & cb(X) ) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx6xcomp % 58.55/58.69 fof(axiom_16,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx6xcomp(X) % 58.55/58.69 <=> ? [Y0] : ra_Px6(X,Y0) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx7 % 58.55/58.69 fof(axiom_17,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx7(X) % 58.55/58.69 <=> ? [Y0] : ra_Px7(X,Y0) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx7xcomp % 58.55/58.69 fof(axiom_18,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx7xcomp(X) % 58.55/58.69 <=> ( cc(X) % 58.55/58.69 & ca(X) ) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx7xcomp % 58.55/58.69 fof(axiom_19,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx7xcomp(X) % 58.55/58.69 <=> ~ ? [Y] : ra_Px7(X,Y) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx8 % 58.55/58.69 fof(axiom_20,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx8(X) % 58.55/58.69 <=> ~ ? [Y] : ra_Px8(X,Y) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx8xcomp % 58.55/58.69 fof(axiom_21,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx8xcomp(X) % 58.55/58.69 <=> ? [Y0] : ra_Px8(X,Y0) ) ). % 58.55/58.69 % 58.55/58.69 %----Equality ca_Cx8xcomp % 58.55/58.69 fof(axiom_22,axiom, % 58.55/58.69 ! [X] : % 58.55/58.69 ( ca_Cx8xcomp(X) % 58.55/58.69 <=> ( cc(X) % 58.55/58.69 & cb(X) ) ) ). % 58.55/58.69 % 58.55/58.69 %----i2003_11_14_17_20_50869 % 58.55/58.69 fof(axiom_23,axiom, % 58.55/58.69 cUnsatisfiable(i2003_11_14_17_20_50869) ). % 58.55/58.69 % 58.55/58.69 %------------------------------------------------------------------------------ % 58.55/58.69 %------------------------------------------- % 58.55/58.69 % Proof found % 58.55/58.69 % SZS status Theorem for theBenchmark % 58.55/58.69 % SZS output start Proof % 58.55/58.69 %ClaNum:50(EqnAxiom:0) % 58.55/58.69 %VarNum:131(SingletonVarNum:63) % 58.55/58.69 %MaxLitNum:4 % 58.55/58.69 %MaxfuncDepth:1 % 58.55/58.69 %SharedTerms:2 % 58.55/58.69 [1]P1(a1) % 58.55/58.69 [2]~P2(x21) % 58.55/58.69 [3]P18(x31)+P17(x31) % 58.55/58.69 [4]~P4(x41)+P3(x41) % 58.55/58.69 [5]~P4(x51)+P10(x51) % 58.55/58.69 [6]~P4(x61)+P5(x61) % 58.55/58.69 [7]~P9(x71)+P6(x71) % 58.55/58.69 [8]~P11(x81)+P6(x81) % 58.55/58.69 [9]~P6(x91)+P7(x91) % 58.55/58.69 [10]~P9(x101)+P12(x101) % 58.55/58.69 [11]~P13(x111)+P12(x111) % 58.55/58.69 [12]~P7(x121)+P14(x121) % 58.55/58.69 [13]~P12(x131)+P14(x131) % 58.55/58.69 [14]~P7(x141)+P15(x141) % 58.55/58.69 [15]~P11(x151)+P16(x151) % 58.55/58.69 [16]~P13(x161)+P16(x161) % 58.55/58.69 [17]~P18(x171)+~P17(x171) % 58.55/58.69 [22]P1(x221)+P19(x221,f2(x221)) % 58.55/58.69 [23]P10(x231)+P23(x231,f3(x231)) % 58.55/58.69 [24]P5(x241)+P24(x241,f8(x241)) % 58.55/58.69 [25]P14(x251)+P20(x251,f9(x251)) % 58.55/58.69 [26]P15(x261)+P22(x261,f10(x261)) % 58.55/58.69 [27]P8(x271)+P21(x271,f14(x271)) % 58.55/58.69 [28]P11(x281)+P25(x281,f4(x281)) % 58.55/58.69 [37]~P4(x371)+P19(x371,f11(x371)) % 58.55/58.69 [38]~P12(x381)+P22(x381,f12(x381)) % 58.55/58.69 [39]~P16(x391)+P20(x391,f13(x391)) % 58.55/58.69 [40]~P7(x401)+P21(x401,f15(x401)) % 58.55/58.69 [41]~P9(x411)+P24(x411,f5(x411)) % 58.55/58.69 [42]~P3(x421)+P25(x421,f6(x421)) % 58.55/58.70 [43]~P13(x431)+P23(x431,f7(x431)) % 58.55/58.70 [30]P4(x301)+~P19(x301,x302) % 58.55/58.70 [31]P3(x311)+~P25(x311,x312) % 58.55/58.70 [32]P7(x321)+~P21(x321,x322) % 58.55/58.70 [33]P12(x331)+~P22(x331,x332) % 58.55/58.70 [34]P16(x341)+~P20(x341,x342) % 58.55/58.70 [35]P9(x351)+~P24(x351,x352) % 58.55/58.70 [36]P13(x361)+~P23(x361,x362) % 58.55/58.70 [44]~P1(x441)+~P19(x441,x442) % 58.55/58.70 [45]~P10(x451)+~P23(x451,x452) % 58.55/58.70 [46]~P5(x461)+~P24(x461,x462) % 58.55/58.70 [47]~P14(x471)+~P20(x471,x472) % 58.55/58.70 [48]~P15(x481)+~P22(x481,x482) % 58.55/58.70 [49]~P8(x491)+~P21(x491,x492) % 58.55/58.70 [50]~P11(x501)+~P25(x501,x502) % 58.55/58.70 [18]~P14(x181)+~P15(x181)+P7(x181) % 58.55/58.70 [19]~P6(x191)+~P12(x191)+P9(x191) % 58.55/58.70 [20]~P6(x201)+~P16(x201)+P11(x201) % 58.55/58.70 [21]~P12(x211)+~P16(x211)+P13(x211) % 58.55/58.70 [29]~P3(x291)+~P10(x291)+~P5(x291)+P4(x291) % 58.55/58.70 %EqnAxiom % 58.55/58.70 % 58.55/58.70 %------------------------------------------- % 58.55/58.74 cnf(53,plain, % 58.55/58.74 (~P4(a1)), % 58.55/58.74 inference(scs_inference,[],[1,44,37])). % 58.55/58.74 cnf(59,plain, % 58.55/58.74 (P7(x591)+~P9(x591)), % 58.55/58.74 inference(scs_inference,[],[7,9])). % 58.55/58.74 cnf(62,plain, % 58.55/58.74 (~P13(x621)+P22(x621,f12(x621))), % 58.55/58.74 inference(scs_inference,[],[11,38])). % 58.55/58.74 cnf(64,plain, % 58.55/58.74 (~P7(x641)+~P22(x641,x642)), % 58.55/58.74 inference(scs_inference,[],[14,48])). % 58.55/58.74 cnf(67,plain, % 58.55/58.74 (P7(x671)+~P24(x671,x672)), % 58.55/58.74 inference(scs_inference,[],[59,35])). % 58.55/58.74 cnf(72,plain, % 58.55/58.74 (P14(x721)+~P21(x721,x722)), % 58.55/58.74 inference(scs_inference,[],[32,12])). % 58.55/58.74 cnf(81,plain, % 58.55/58.74 (~P22(x811,x812)+~P24(x811,x813)), % 58.55/58.74 inference(scs_inference,[],[64,67])). % 58.55/58.74 cnf(83,plain, % 58.55/58.74 (~P21(x831,x832)+~P20(x831,x833)), % 58.55/58.74 inference(scs_inference,[],[72,47])). % 58.55/58.74 cnf(93,plain, % 58.55/58.74 (~P6(x931)+P21(x931,f15(x931))), % 58.55/58.74 inference(scs_inference,[],[40,9])). % 58.55/58.74 cnf(95,plain, % 58.55/58.74 (~P23(x951,x952)+P23(x951,f7(x951))), % 58.55/58.74 inference(scs_inference,[],[43,36])). % 58.55/58.74 cnf(96,plain, % 58.55/58.74 (~P13(x961)+~P7(x961)), % 58.55/58.74 inference(scs_inference,[],[62,64])). % 58.55/58.74 cnf(97,plain, % 58.55/58.74 (~P13(x971)+~P21(x971,x972)), % 58.55/58.74 inference(scs_inference,[],[96,32])). % 58.55/58.74 cnf(98,plain, % 58.55/58.74 (~P21(x981,x982)+~P23(x981,x983)), % 58.55/58.74 inference(scs_inference,[],[97,36])). % 58.55/58.74 cnf(115,plain, % 58.55/58.74 (~P12(x1151)+~P24(x1151,x1152)), % 58.55/58.74 inference(scs_inference,[],[81,38])). % 58.55/58.74 cnf(116,plain, % 58.55/58.74 (~P24(x1161,x1162)+~P9(x1161)), % 58.55/58.74 inference(scs_inference,[],[115,10])). % 58.55/58.74 cnf(117,plain, % 58.55/58.74 (~P24(x1171,x1172)+~P24(x1171,x1173)), % 58.55/58.74 inference(scs_inference,[],[116,35])). % 58.55/58.74 cnf(118,plain, % 58.55/58.74 (P8(x1181)+~P20(x1181,x1182)), % 58.55/58.74 inference(scs_inference,[],[83,27])). % 58.55/58.74 cnf(119,plain, % 58.55/58.74 (P8(x1191)+~P16(x1191)), % 58.55/58.74 inference(scs_inference,[],[118,39])). % 58.55/58.74 cnf(120,plain, % 58.55/58.74 (P8(x1201)+~P11(x1201)), % 58.55/58.74 inference(scs_inference,[],[119,15])). % 58.55/58.74 cnf(121,plain, % 58.55/58.74 (P8(x1211)+P25(x1211,f4(x1211))), % 58.55/58.74 inference(scs_inference,[],[120,28])). % 58.55/58.74 cnf(124,plain, % 58.55/58.74 (~P6(x1241)+~P8(x1241)), % 58.55/58.74 inference(scs_inference,[],[93,49])). % 58.55/58.74 cnf(125,plain, % 58.55/58.74 (P25(x1251,f4(x1251))+~P6(x1251)), % 58.55/58.74 inference(scs_inference,[],[124,121])). % 58.55/58.74 cnf(126,plain, % 58.55/58.74 (P8(x1261)+~P23(x1261,x1262)), % 58.55/58.74 inference(scs_inference,[],[98,27])). % 58.55/58.74 cnf(127,plain, % 58.55/58.74 (P8(x1271)+P10(x1271)), % 58.55/58.74 inference(scs_inference,[],[126,23])). % 58.55/58.74 cnf(128,plain, % 58.55/58.74 (~P5(a1)+P8(a1)+~P3(a1)), % 58.55/58.74 inference(scs_inference,[],[53,127,29])). % 58.55/58.74 cnf(133,plain, % 58.55/58.74 (P25(x1331,f4(x1331))+~P11(x1331)), % 58.55/58.74 inference(scs_inference,[],[125,8])). % 58.55/58.74 cnf(135,plain, % 58.55/58.74 (P25(x1351,f4(x1351))), % 58.55/58.74 inference(scs_inference,[],[133,28])). % 58.55/58.74 cnf(161,plain, % 58.55/58.74 (P23(x1611,f7(x1611))+P10(x1611)), % 58.55/58.74 inference(scs_inference,[],[95,23])). % 58.55/58.74 cnf(162,plain, % 58.55/58.74 (~P5(a1)+P23(a1,f7(a1))+~P3(a1)), % 58.55/58.74 inference(scs_inference,[],[53,161,29])). % 58.55/58.74 cnf(167,plain, % 58.55/58.74 (P24(a1,f8(a1))+P8(a1)+~P3(a1)), % 58.55/58.74 inference(scs_inference,[],[128,24])). % 58.55/58.74 cnf(189,plain, % 58.55/58.74 (P13(a1)+~P5(a1)+~P3(a1)), % 58.55/58.74 inference(scs_inference,[],[162,36])). % 58.55/58.74 cnf(196,plain, % 58.55/58.74 (P8(a1)+~P3(a1)), % 58.55/58.74 inference(scs_inference,[],[167,117])). % 58.55/58.74 cnf(197,plain, % 58.55/58.74 (~P21(a1,x1971)+~P3(a1)), % 58.55/58.74 inference(scs_inference,[],[196,49])). % 58.55/58.74 cnf(198,plain, % 58.55/58.74 (~P7(a1)+~P3(a1)), % 58.55/58.74 inference(scs_inference,[],[197,40])). % 58.55/58.74 cnf(3375,plain, % 58.55/58.74 (P3(x33751)), % 58.55/58.74 inference(scs_inference,[],[135,31])). % 58.55/58.74 cnf(3387,plain, % 58.55/58.74 (P23(a1,f7(a1))+~P5(a1)), % 58.55/58.74 inference(scs_inference,[],[3375,162])). % 58.55/58.74 cnf(3388,plain, % 58.55/58.74 (P13(a1)+~P5(a1)), % 58.55/58.74 inference(scs_inference,[],[3375,189])). % 58.55/58.74 cnf(3390,plain, % 58.55/58.74 (~P7(a1)), % 58.55/58.74 inference(scs_inference,[],[3375,198])). % 58.55/58.74 cnf(3394,plain, % 58.55/58.74 (P16(a1)+~P5(a1)), % 58.55/58.74 inference(scs_inference,[],[3388,16])). % 58.55/58.74 cnf(3396,plain, % 58.55/58.74 (P20(a1,f13(a1))+~P5(a1)), % 58.55/58.74 inference(scs_inference,[],[3394,39])). % 58.55/58.74 cnf(3397,plain, % 58.55/58.74 (~P10(a1)+~P5(a1)), % 58.55/58.74 inference(scs_inference,[],[3387,45])). % 58.55/58.74 cnf(3403,plain, % 58.55/58.74 (~P14(a1)+~P5(a1)), % 58.55/58.74 inference(scs_inference,[],[3396,47])). % 58.55/58.74 cnf(3404,plain, % 58.55/58.74 (~P12(a1)+~P5(a1)), % 58.55/58.74 inference(scs_inference,[],[3403,13])). % 58.55/58.74 cnf(3405,plain, % 58.55/58.74 (~P13(a1)+~P5(a1)), % 58.55/58.74 inference(scs_inference,[],[3404,11])). % 58.55/58.74 cnf(3406,plain, % 58.55/58.74 (~P23(a1,x34061)+~P5(a1)), % 58.55/58.74 inference(scs_inference,[],[3405,36])). % 58.55/58.74 cnf(3407,plain, % 58.55/58.74 (P10(a1)+~P5(a1)), % 58.55/58.74 inference(scs_inference,[],[3406,161])). % 58.55/58.74 cnf(3408,plain, % 58.55/58.74 (~P5(a1)), % 58.55/58.74 inference(scs_inference,[],[3407,3397])). % 58.55/58.74 cnf(65508,plain, % 58.55/58.74 ($false), % 58.55/58.74 inference(scs_inference,[],[3408,3390,24,117]), % 58.55/58.74 ['proof']). % 58.69/58.80 % SZS output end Proof % 58.69/58.80 % Total time :58.000000s %------------------------------------------------------------------------------