%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MSC010+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 : n021.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 11:52:12 EDT 2024 % Result : Theorem 0.53s 0.67s % Output : CNFRefutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : MSC010+1 : TPTP v8.2.0. Released v3.1.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n021.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 : Sat Jun 22 05:46:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 0.53/0.66 %------------------------------------------- % 0.53/0.66 % File :CSE---1.7 % 0.53/0.66 % Problem :theBenchmark % 0.53/0.66 % Transform :cnf % 0.53/0.66 % Format :tptp:raw % 0.53/0.66 % Command :java -jar mcs_scs.jar %d %s % 0.53/0.66 % 0.53/0.66 % Result :Theorem 0.010000s % 0.53/0.66 % Output :CNFRefutation 0.010000s % 0.53/0.66 %------------------------------------------- % 0.53/0.66 %------------------------------------------------------------------------------ % 0.53/0.66 % File : MSC010+1 : TPTP v8.2.0. Released v3.1.0. % 0.53/0.66 % Domain : Miscellaneous % 0.53/0.66 % Problem : Simple, but hard, obligation from proof verification % 0.53/0.66 % Version : Especial. % 0.53/0.66 % English : Verification of the negation of a conjecture, which is simply to % 0.53/0.66 % prove the double negated version of a formula from the formula. % 0.53/0.66 % 0.53/0.66 % Refs : % 0.53/0.66 % Source : [TPTP] % 0.53/0.66 % Names : % 0.53/0.66 % 0.53/0.66 % Status : Theorem % 0.53/0.66 % Rating : 0.25 v8.2.0, 0.22 v7.4.0, 0.23 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.23 v6.4.0, 0.27 v6.3.0, 0.25 v6.2.0, 0.32 v6.1.0, 0.33 v6.0.0, 0.22 v5.5.0, 0.33 v5.4.0, 0.39 v5.3.0, 0.52 v5.2.0, 0.35 v5.1.0, 0.38 v5.0.0, 0.42 v4.1.0, 0.48 v4.0.0, 0.50 v3.7.0, 0.45 v3.5.0, 0.47 v3.4.0, 0.58 v3.3.0, 0.57 v3.2.0, 0.82 v3.1.0 % 0.53/0.66 % Syntax : Number of formulae : 2 ( 0 unt; 0 def) % 0.53/0.66 % Number of atoms : 136 ( 30 equ) % 0.53/0.66 % Maximal formula atoms : 68 ( 68 avg) % 0.53/0.66 % Number of connectives : 140 ( 6 ~; 0 |; 102 &) % 0.53/0.66 % ( 0 <=>; 32 =>; 0 <=; 0 <~>) % 0.53/0.66 % Maximal formula depth : 26 ( 25 avg) % 0.53/0.66 % Maximal term depth : 2 ( 1 avg) % 0.53/0.66 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty) % 0.53/0.66 % Number of functors : 18 ( 18 usr; 16 con; 0-3 aty) % 0.53/0.66 % Number of variables : 44 ( 44 !; 0 ?) % 0.53/0.66 % SPC : FOF_THM_RFO_SEQ % 0.53/0.66 % 0.53/0.66 % Comments : % 0.53/0.66 %------------------------------------------------------------------------------ % 0.53/0.66 fof(n1,axiom, % 0.53/0.66 ( ( pv63 != pv64 % 0.53/0.66 & leq(n0,pv5) % 0.53/0.66 & leq(n0,pv63) % 0.53/0.66 & leq(n0,pv64) % 0.53/0.66 & leq(pv5,n998) % 0.53/0.66 & leq(pv63,n5) % 0.53/0.66 & leq(pv64,n5) % 0.53/0.66 & ! [X1,X2] : % 0.53/0.66 ( ( leq(n0,X1) % 0.53/0.66 & leq(n0,X2) % 0.53/0.66 & leq(X1,n2) % 0.53/0.66 & leq(X2,n5) ) % 0.53/0.66 => a_select3(h_ds1_filter_init,X1,X2) = init ) % 0.53/0.67 & ! [X3,X4] : % 0.53/0.67 ( ( leq(n0,X3) % 0.53/0.67 & leq(n0,X4) % 0.53/0.67 & leq(X3,n5) % 0.53/0.67 & leq(X4,n5) ) % 0.53/0.67 => a_select3(phi_ds1_filter_init,X3,X4) = init ) % 0.53/0.67 & ! [X5,X6] : % 0.53/0.67 ( ( leq(n0,X5) % 0.53/0.67 & leq(n0,X6) % 0.53/0.67 & leq(X5,n5) % 0.53/0.67 & leq(X6,n0) ) % 0.53/0.67 => a_select3(dv_ds1_filter_init,X5,X6) = init ) % 0.53/0.67 & ! [X7,X8] : % 0.53/0.67 ( ( leq(n0,X7) % 0.53/0.67 & leq(n0,X8) % 0.53/0.67 & leq(X7,n5) % 0.53/0.67 & leq(X8,n5) ) % 0.53/0.67 => a_select3(q_ds1_filter_init,X7,X8) = init ) % 0.53/0.67 & ! [X9,X10] : % 0.53/0.67 ( ( leq(n0,X9) % 0.53/0.67 & leq(n0,X10) % 0.53/0.67 & leq(X9,n2) % 0.53/0.67 & leq(X10,n2) ) % 0.53/0.67 => a_select3(r_ds1_filter_init,X9,X10) = init ) % 0.53/0.67 & ! [X11,X12] : % 0.53/0.67 ( ( leq(n0,X11) % 0.53/0.67 & leq(n0,X12) % 0.53/0.67 & leq(X11,n5) % 0.53/0.67 & leq(X12,n0) ) % 0.53/0.67 => a_select3(xhatmin_ds1_filter_init,X11,X12) = init ) % 0.53/0.67 & ! [X13,X14] : % 0.53/0.67 ( ( leq(n0,X13) % 0.53/0.67 & leq(n0,X14) % 0.53/0.67 & leq(X13,n5) % 0.53/0.67 & leq(X14,n5) ) % 0.53/0.67 => a_select3(pminus_ds1_filter_init,X13,X14) = init ) % 0.53/0.67 & ! [X15,X16] : % 0.53/0.67 ( ( leq(n0,X15) % 0.53/0.67 & leq(n0,X16) % 0.53/0.67 & leq(X15,n5) % 0.53/0.67 & leq(X16,n5) ) % 0.53/0.67 => ( ( X15 = pv63 % 0.53/0.67 & gt(pv64,X16) ) % 0.53/0.67 => a_select3(id_ds1_filter_init,X15,X16) = init ) ) % 0.53/0.67 & ! [X17,X18] : % 0.53/0.67 ( ( leq(n0,X17) % 0.53/0.67 & leq(n0,X18) % 0.53/0.67 & leq(X17,n5) % 0.53/0.67 & leq(X18,n5) ) % 0.53/0.67 => ( gt(pv63,X17) % 0.53/0.67 => a_select3(id_ds1_filter_init,X17,X18) = init ) ) % 0.53/0.67 & ! [X19] : % 0.53/0.67 ( ( leq(n0,X19) % 0.53/0.67 & leq(X19,pred(pv63)) ) % 0.53/0.67 => ! [X20] : % 0.53/0.67 ( ( leq(n0,X20) % 0.53/0.67 & leq(X20,n5) ) % 0.53/0.67 => a_select3(id_ds1_filter_init,X19,X20) = init ) ) ) % 0.53/0.67 => ! [X21,X22] : % 0.53/0.67 ( ( leq(n0,X21) % 0.53/0.67 & leq(n0,X22) % 0.53/0.67 & leq(X21,n5) % 0.53/0.67 & leq(X22,n5) ) % 0.53/0.67 => ( ( pv64 != X22 % 0.53/0.67 & X21 = pv63 % 0.53/0.67 & leq(X22,pv64) ) % 0.53/0.67 => a_select3(id_ds1_filter_init,X21,X22) = init ) ) ) ). % 0.53/0.67 % 0.53/0.67 fof(n91,conjecture, % 0.53/0.67 ~ ~ ( ( pv63 != pv64 % 0.53/0.67 & leq(n0,pv5) % 0.53/0.67 & leq(n0,pv63) % 0.53/0.67 & leq(n0,pv64) % 0.53/0.67 & leq(pv5,n998) % 0.53/0.67 & leq(pv63,n5) % 0.53/0.67 & leq(pv64,n5) % 0.53/0.67 & ! [X1,X2] : % 0.53/0.67 ( ( leq(n0,X1) % 0.53/0.67 & leq(n0,X2) % 0.53/0.67 & leq(X1,n2) % 0.53/0.67 & leq(X2,n5) ) % 0.53/0.67 => a_select3(h_ds1_filter_init,X1,X2) = init ) % 0.53/0.67 & ! [X3,X4] : % 0.53/0.67 ( ( leq(n0,X3) % 0.53/0.67 & leq(n0,X4) % 0.53/0.67 & leq(X3,n5) % 0.53/0.67 & leq(X4,n5) ) % 0.53/0.67 => a_select3(phi_ds1_filter_init,X3,X4) = init ) % 0.53/0.67 & ! [X5,X6] : % 0.53/0.67 ( ( leq(n0,X5) % 0.53/0.67 & leq(n0,X6) % 0.53/0.67 & leq(X5,n5) % 0.53/0.67 & leq(X6,n0) ) % 0.53/0.67 => a_select3(dv_ds1_filter_init,X5,X6) = init ) % 0.53/0.67 & ! [X7,X8] : % 0.53/0.67 ( ( leq(n0,X7) % 0.53/0.67 & leq(n0,X8) % 0.53/0.67 & leq(X7,n5) % 0.53/0.67 & leq(X8,n5) ) % 0.53/0.67 => a_select3(q_ds1_filter_init,X7,X8) = init ) % 0.53/0.67 & ! [X9,X10] : % 0.53/0.67 ( ( leq(n0,X9) % 0.53/0.67 & leq(n0,X10) % 0.53/0.67 & leq(X9,n2) % 0.53/0.67 & leq(X10,n2) ) % 0.53/0.67 => a_select3(r_ds1_filter_init,X9,X10) = init ) % 0.53/0.67 & ! [X11,X12] : % 0.53/0.67 ( ( leq(n0,X11) % 0.53/0.67 & leq(n0,X12) % 0.53/0.67 & leq(X11,n5) % 0.53/0.67 & leq(X12,n0) ) % 0.53/0.67 => a_select3(xhatmin_ds1_filter_init,X11,X12) = init ) % 0.53/0.67 & ! [X13,X14] : % 0.53/0.67 ( ( leq(n0,X13) % 0.53/0.67 & leq(n0,X14) % 0.53/0.67 & leq(X13,n5) % 0.53/0.67 & leq(X14,n5) ) % 0.53/0.67 => a_select3(pminus_ds1_filter_init,X13,X14) = init ) % 0.53/0.67 & ! [X15,X16] : % 0.53/0.67 ( ( leq(n0,X15) % 0.53/0.67 & leq(n0,X16) % 0.53/0.67 & leq(X15,n5) % 0.53/0.67 & leq(X16,n5) ) % 0.53/0.67 => ( ( X15 = pv63 % 0.53/0.67 & gt(pv64,X16) ) % 0.53/0.67 => a_select3(id_ds1_filter_init,X15,X16) = init ) ) % 0.53/0.67 & ! [X17,X18] : % 0.53/0.67 ( ( leq(n0,X17) % 0.53/0.67 & leq(n0,X18) % 0.53/0.67 & leq(X17,n5) % 0.53/0.67 & leq(X18,n5) ) % 0.53/0.67 => ( gt(pv63,X17) % 0.53/0.67 => a_select3(id_ds1_filter_init,X17,X18) = init ) ) % 0.53/0.67 & ! [X19] : % 0.53/0.67 ( ( leq(n0,X19) % 0.53/0.67 & leq(X19,pred(pv63)) ) % 0.53/0.67 => ! [X20] : % 0.53/0.67 ( ( leq(n0,X20) % 0.53/0.67 & leq(X20,n5) ) % 0.53/0.67 => a_select3(id_ds1_filter_init,X19,X20) = init ) ) ) % 0.53/0.67 => ! [X21,X22] : % 0.53/0.67 ( ( leq(n0,X21) % 0.53/0.67 & leq(n0,X22) % 0.53/0.67 & leq(X21,n5) % 0.53/0.67 & leq(X22,n5) ) % 0.53/0.67 => ( ( pv64 != X22 % 0.53/0.67 & X21 = pv63 % 0.53/0.67 & leq(X22,pv64) ) % 0.53/0.67 => a_select3(id_ds1_filter_init,X21,X22) = init ) ) ) ). % 0.53/0.67 % 0.53/0.67 %------------------------------------------------------------------------------ % 0.53/0.67 %------------------------------------------- % 0.53/0.67 % Proof found % 0.53/0.67 % SZS status Theorem for theBenchmark % 0.53/0.67 % SZS output start Proof % 0.53/0.67 %ClaNum:187(EqnAxiom:16) % 0.53/0.67 %VarNum:72(SingletonVarNum:22) % 0.53/0.67 %MaxLitNum:10 % 0.53/0.67 %MaxfuncDepth:1 % 0.53/0.67 %SharedTerms:136 % 0.53/0.67 %goalClause: 17 18 19 20 21 22 23 24 25 % 0.53/0.67 %singleGoalClaCount:9 % 0.53/0.67 [17]E(a1,a14) % 0.53/0.67 [18]P1(a5000) % 0.53/0.67 [19]P6(a15,a1) % 0.53/0.67 [20]P6(a15,a16) % 0.53/0.67 [21]P6(a1,a30) % 0.53/0.67 [22]P6(a16,a37) % 0.53/0.67 [23]P6(a16,a30) % 0.53/0.67 [24]~E(a37,a16) % 0.53/0.67 [25]~E(f2(a20,a1,a16),a29) % 0.53/0.67 [26]P2(a5000)+~P3(a5000) % 0.53/0.67 [27]P3(a5000)+~P4(a5000) % 0.53/0.67 [28]P4(a5000)+~P5(a5000) % 0.53/0.67 [29]P5(a5000)+~P1(a5000) % 0.53/0.67 [30]~E(a37,a14)+~P2(a5000) % 0.53/0.67 [31]P6(a14,a30)+~P2(a5000) % 0.53/0.67 [32]P6(a37,a30)+~P2(a5000) % 0.53/0.67 [33]P6(a15,a14)+~P2(a5000) % 0.53/0.67 [34]P6(a15,a37)+~P2(a5000) % 0.53/0.67 [35]P6(a15,a32)+~P2(a5000) % 0.53/0.67 [36]P6(a32,a33)+~P2(a5000) % 0.53/0.67 [37]E(a3,a14)+P5(a5000)+P6(a15,a4)+~P4(a5000) % 0.53/0.67 [38]E(a3,a14)+P5(a5000)+P6(a15,a11)+~P4(a5000) % 0.53/0.67 [39]E(a3,a14)+P5(a5000)+P6(a4,a30)+~P4(a5000) % 0.53/0.67 [40]E(a3,a14)+P5(a5000)+P6(a11,a30)+~P4(a5000) % 0.53/0.67 [41]P3(a5000)+P6(a15,a21)+P6(a15,a26)+~P2(a5000) % 0.53/0.67 [42]P6(a15,a21)+P3(a5000)+P6(a15,a5)+~P2(a5000) % 0.53/0.67 [43]P6(a15,a21)+P3(a5000)+P6(a26,a30)+~P2(a5000) % 0.53/0.67 [44]P6(a15,a21)+P3(a5000)+P6(a5,a30)+~P2(a5000) % 0.53/0.67 [45]P6(a15,a26)+P3(a5000)+P6(a15,a27)+~P2(a5000) % 0.53/0.67 [46]P6(a15,a27)+P6(a15,a5)+P3(a5000)+~P2(a5000) % 0.53/0.67 [47]P6(a15,a27)+P6(a26,a30)+P3(a5000)+~P2(a5000) % 0.53/0.67 [48]P6(a15,a27)+P6(a5,a30)+P3(a5000)+~P2(a5000) % 0.53/0.67 [49]P6(a15,a26)+P3(a5000)+P6(a21,a30)+~P2(a5000) % 0.53/0.67 [50]P6(a15,a26)+P3(a5000)+P6(a27,a15)+~P2(a5000) % 0.53/0.67 [51]P6(a15,a5)+P6(a21,a30)+P3(a5000)+~P2(a5000) % 0.53/0.67 [52]P6(a15,a5)+P6(a27,a15)+P3(a5000)+~P2(a5000) % 0.53/0.67 [53]P6(a21,a30)+P6(a26,a30)+P3(a5000)+~P2(a5000) % 0.53/0.67 [54]P6(a21,a30)+P6(a5,a30)+P3(a5000)+~P2(a5000) % 0.53/0.67 [55]P6(a26,a30)+P6(a27,a15)+P3(a5000)+~P2(a5000) % 0.53/0.67 [56]P6(a27,a15)+P6(a5,a30)+P3(a5000)+~P2(a5000) % 0.53/0.67 [57]P4(a5000)+P6(a15,a7)+P6(a15,a8)+~P3(a5000) % 0.53/0.67 [58]P6(a15,a7)+P4(a5000)+P6(a15,a10)+~P3(a5000) % 0.53/0.67 [59]P6(a15,a7)+P4(a5000)+P6(a8,a30)+~P3(a5000) % 0.53/0.67 [60]P6(a15,a7)+P4(a5000)+P6(a10,a15)+~P3(a5000) % 0.53/0.67 [61]P6(a15,a8)+P4(a5000)+P6(a15,a9)+~P3(a5000) % 0.53/0.67 [62]P6(a15,a9)+P6(a15,a10)+P4(a5000)+~P3(a5000) % 0.53/0.67 [63]P6(a15,a9)+P6(a8,a30)+P4(a5000)+~P3(a5000) % 0.53/0.67 [64]P6(a15,a9)+P6(a10,a15)+P4(a5000)+~P3(a5000) % 0.53/0.67 [65]P6(a15,a8)+P4(a5000)+P6(a7,a31)+~P3(a5000) % 0.53/0.67 [66]P6(a15,a8)+P4(a5000)+P6(a9,a31)+~P3(a5000) % 0.53/0.67 [67]P6(a15,a10)+P6(a7,a31)+P4(a5000)+~P3(a5000) % 0.53/0.67 [68]P6(a15,a10)+P6(a9,a31)+P4(a5000)+~P3(a5000) % 0.53/0.67 [69]P6(a7,a31)+P6(a8,a30)+P4(a5000)+~P3(a5000) % 0.53/0.67 [70]P6(a7,a31)+P6(a10,a15)+P4(a5000)+~P3(a5000) % 0.53/0.67 [71]P6(a8,a30)+P6(a9,a31)+P4(a5000)+~P3(a5000) % 0.53/0.67 [72]P6(a9,a31)+P6(a10,a15)+P4(a5000)+~P3(a5000) % 0.53/0.67 [73]P6(a15,a4)+P5(a5000)+P6(a15,a3)+~P4(a5000) % 0.53/0.67 [74]P6(a15,a4)+P5(a5000)+P6(a15,a12)+~P4(a5000) % 0.53/0.67 [75]P6(a15,a4)+P5(a5000)+P6(a3,a30)+~P4(a5000) % 0.53/0.67 [76]P6(a15,a4)+P5(a5000)+P6(a12,a30)+~P4(a5000) % 0.53/0.67 [77]P6(a15,a4)+P5(a5000)+P7(a37,a12)+~P4(a5000) % 0.53/0.67 [78]P6(a15,a11)+P6(a15,a3)+P5(a5000)+~P4(a5000) % 0.53/0.67 [79]P6(a15,a11)+P6(a15,a12)+P5(a5000)+~P4(a5000) % 0.53/0.67 [80]P6(a15,a11)+P6(a3,a30)+P5(a5000)+~P4(a5000) % 0.53/0.67 [81]P6(a15,a11)+P6(a12,a30)+P5(a5000)+~P4(a5000) % 0.53/0.67 [82]P6(a15,a11)+P7(a37,a12)+P5(a5000)+~P4(a5000) % 0.53/0.67 [83]P6(a15,a3)+P6(a4,a30)+P5(a5000)+~P4(a5000) % 0.53/0.67 [84]P6(a15,a3)+P6(a11,a30)+P5(a5000)+~P4(a5000) % 0.53/0.67 [85]P6(a15,a12)+P6(a4,a30)+P5(a5000)+~P4(a5000) % 0.53/0.67 [86]P6(a15,a12)+P6(a11,a30)+P5(a5000)+~P4(a5000) % 0.53/0.67 [87]P6(a4,a30)+P6(a3,a30)+P5(a5000)+~P4(a5000) % 0.53/0.67 [88]P6(a4,a30)+P6(a12,a30)+P5(a5000)+~P4(a5000) % 0.53/0.67 [89]P6(a4,a30)+P7(a37,a12)+P5(a5000)+~P4(a5000) % 0.53/0.67 [90]P6(a11,a30)+P6(a3,a30)+P5(a5000)+~P4(a5000) % 0.53/0.67 [91]P6(a11,a30)+P6(a12,a30)+P5(a5000)+~P4(a5000) % 0.53/0.67 [92]P6(a11,a30)+P7(a37,a12)+P5(a5000)+~P4(a5000) % 0.53/0.67 [113]E(a3,a14)+P5(a5000)+~P4(a5000)+~E(f2(a35,a4,a11),a29) % 0.53/0.67 [114]P6(a15,a21)+P3(a5000)+~P2(a5000)+~E(f2(a38,a26,a5),a29) % 0.53/0.67 [115]P6(a15,a27)+P3(a5000)+~P2(a5000)+~E(f2(a38,a26,a5),a29) % 0.53/0.67 [116]P6(a15,a26)+P3(a5000)+~P2(a5000)+~E(f2(a6,a21,a27),a29) % 0.53/0.67 [117]P6(a15,a5)+P3(a5000)+~P2(a5000)+~E(f2(a6,a21,a27),a29) % 0.53/0.67 [118]P6(a21,a30)+P3(a5000)+~P2(a5000)+~E(f2(a38,a26,a5),a29) % 0.53/0.67 [119]P6(a27,a15)+P3(a5000)+~P2(a5000)+~E(f2(a38,a26,a5),a29) % 0.53/0.67 [120]P6(a26,a30)+P3(a5000)+~P2(a5000)+~E(f2(a6,a21,a27),a29) % 0.53/0.67 [121]P6(a5,a30)+P3(a5000)+~P2(a5000)+~E(f2(a6,a21,a27),a29) % 0.53/0.67 [122]P6(a15,a7)+P4(a5000)+~P3(a5000)+~E(f2(a39,a8,a10),a29) % 0.53/0.67 [123]P6(a15,a9)+P4(a5000)+~P3(a5000)+~E(f2(a39,a8,a10),a29) % 0.53/0.67 [124]P6(a15,a8)+P4(a5000)+~P3(a5000)+~E(f2(a40,a7,a9),a29) % 0.53/0.67 [125]P6(a15,a10)+P4(a5000)+~P3(a5000)+~E(f2(a40,a7,a9),a29) % 0.53/0.67 [126]P6(a7,a31)+P4(a5000)+~P3(a5000)+~E(f2(a39,a8,a10),a29) % 0.53/0.67 [127]P6(a9,a31)+P4(a5000)+~P3(a5000)+~E(f2(a39,a8,a10),a29) % 0.53/0.67 [128]P6(a8,a30)+P4(a5000)+~P3(a5000)+~E(f2(a40,a7,a9),a29) % 0.53/0.67 [129]P6(a10,a15)+P4(a5000)+~P3(a5000)+~E(f2(a40,a7,a9),a29) % 0.53/0.67 [130]P6(a15,a4)+P5(a5000)+~P4(a5000)+~E(f2(a20,a3,a12),a29) % 0.53/0.67 [131]P6(a15,a11)+P5(a5000)+~P4(a5000)+~E(f2(a20,a3,a12),a29) % 0.53/0.67 [132]P6(a15,a3)+P5(a5000)+~P4(a5000)+~E(f2(a35,a4,a11),a29) % 0.53/0.67 [133]P6(a15,a12)+P5(a5000)+~P4(a5000)+~E(f2(a35,a4,a11),a29) % 0.53/0.67 [134]P6(a4,a30)+P5(a5000)+~P4(a5000)+~E(f2(a20,a3,a12),a29) % 0.53/0.67 [135]P6(a11,a30)+P5(a5000)+~P4(a5000)+~E(f2(a20,a3,a12),a29) % 0.53/0.67 [136]P6(a3,a30)+P5(a5000)+~P4(a5000)+~E(f2(a35,a4,a11),a29) % 0.53/0.67 [137]P6(a12,a30)+P5(a5000)+~P4(a5000)+~E(f2(a35,a4,a11),a29) % 0.53/0.67 [138]P7(a37,a12)+P5(a5000)+~P4(a5000)+~E(f2(a35,a4,a11),a29) % 0.53/0.67 [174]P3(a5000)+~P2(a5000)+~E(f2(a6,a21,a27),a29)+~E(f2(a38,a26,a5),a29) % 0.53/0.67 [175]P4(a5000)+~P3(a5000)+~E(f2(a40,a7,a9),a29)+~E(f2(a39,a8,a10),a29) % 0.53/0.67 [176]P5(a5000)+~P4(a5000)+~E(f2(a35,a4,a11),a29)+~E(f2(a20,a3,a12),a29) % 0.53/0.67 [164]~P6(x1642,a30)+~P6(x1641,a31)+~P6(a15,x1642)+~P6(a15,x1641)+~P2(a5000)+E(f2(a28,x1641,x1642),a29) % 0.53/0.67 [165]~P6(x1652,a30)+~P6(x1651,a30)+~P6(a15,x1652)+~P6(a15,x1651)+~P2(a5000)+E(f2(a36,x1651,x1652),a29) % 0.53/0.67 [166]~P6(x1662,a15)+~P6(x1661,a30)+~P6(a15,x1662)+~P6(a15,x1661)+~P3(a5000)+E(f2(a6,x1661,x1662),a29) % 0.53/0.67 [167]~P6(x1672,a30)+~P6(x1671,a30)+~P6(a15,x1672)+~P6(a15,x1671)+~P3(a5000)+E(f2(a38,x1671,x1672),a29) % 0.53/0.67 [168]~P6(x1682,a31)+~P6(x1681,a31)+~P6(a15,x1682)+~P6(a15,x1681)+~P4(a5000)+E(f2(a40,x1681,x1682),a29) % 0.53/0.67 [169]~P6(x1692,a15)+~P6(x1691,a30)+~P6(a15,x1692)+~P6(a15,x1691)+~P4(a5000)+E(f2(a39,x1691,x1692),a29) % 0.53/0.67 [170]~P6(x1702,a30)+~P6(x1701,a30)+~P6(a15,x1702)+~P6(a15,x1701)+~P5(a5000)+E(f2(a35,x1701,x1702),a29) % 0.53/0.67 [171]~P6(x1712,a30)+~P6(a15,x1712)+~P6(a15,x1711)+~P6(x1711,f34(a14))+~P1(a5000)+E(f2(a20,x1711,x1712),a29) % 0.53/0.67 [172]~P6(x1722,a30)+~P6(x1721,a30)+~P6(a15,x1722)+~P6(a15,x1721)+~P7(a14,x1721)+~P1(a5000)+E(f2(a20,x1721,x1722),a29) % 0.53/0.67 [173]~E(x1731,a14)+~P6(x1732,a30)+~P6(x1731,a30)+~P6(a15,x1732)+~P6(a15,x1731)+~P7(a37,x1732)+~P5(a5000)+E(f2(a20,x1731,x1732),a29) % 0.53/0.67 [178]~E(x1782,a14)+~P6(x1781,a37)+~P6(x1781,a30)+~P6(x1782,a30)+~P6(a15,x1781)+~P6(a15,x1782)+E(a37,x1781)+~P1(a5000)+E(f2(a20,x1782,x1781),a29) % 0.53/0.67 [148]E(a37,a14)+P2(a5000)+P6(a15,a22)+P6(a15,a23)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33) % 0.53/0.67 [149]E(a37,a14)+P6(a15,a22)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P2(a5000)+P6(a15,a25) % 0.53/0.67 [150]E(a37,a14)+P6(a15,a22)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P2(a5000)+P6(a23,a30) % 0.53/0.67 [151]E(a37,a14)+P6(a15,a22)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P2(a5000)+P6(a25,a30) % 0.53/0.67 [152]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a23)+P2(a5000)+P6(a15,a24) % 0.53/0.67 [153]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a24)+P6(a15,a25)+P2(a5000) % 0.53/0.67 [154]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a24)+P6(a23,a30)+P2(a5000) % 0.53/0.67 [155]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a24)+P6(a25,a30)+P2(a5000) % 0.53/0.67 [156]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a23)+P2(a5000)+P6(a22,a31) % 0.53/0.67 [157]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a23)+P2(a5000)+P6(a24,a30) % 0.53/0.67 [158]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a25)+P6(a22,a31)+P2(a5000) % 0.53/0.67 [159]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a25)+P6(a24,a30)+P2(a5000) % 0.53/0.67 [160]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a22,a31)+P6(a23,a30)+P2(a5000) % 0.53/0.67 [161]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a22,a31)+P6(a25,a30)+P2(a5000) % 0.53/0.67 [162]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a23,a30)+P6(a24,a30)+P2(a5000) % 0.53/0.67 [163]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a24,a30)+P6(a25,a30)+P2(a5000) % 0.53/0.67 [179]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a22)+P2(a5000)+~E(f2(a36,a23,a25),a29) % 0.53/0.67 [180]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a24)+P2(a5000)+~E(f2(a36,a23,a25),a29) % 0.53/0.67 [181]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a23)+P2(a5000)+~E(f2(a28,a22,a24),a29) % 0.53/0.67 [182]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a15,a25)+P2(a5000)+~E(f2(a28,a22,a24),a29) % 0.53/0.67 [183]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a22,a31)+P2(a5000)+~E(f2(a36,a23,a25),a29) % 0.53/0.67 [184]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a24,a30)+P2(a5000)+~E(f2(a36,a23,a25),a29) % 0.53/0.67 [185]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a23,a30)+P2(a5000)+~E(f2(a28,a22,a24),a29) % 0.53/0.67 [186]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P6(a25,a30)+P2(a5000)+~E(f2(a28,a22,a24),a29) % 0.53/0.67 [187]E(a37,a14)+~P6(a14,a30)+~P6(a37,a30)+~P6(a15,a14)+~P6(a15,a37)+~P6(a15,a32)+~P6(a32,a33)+P2(a5000)+~E(f2(a28,a22,a24),a29)+~E(f2(a36,a23,a25),a29) % 0.53/0.67 %EqnAxiom % 0.53/0.67 [1]E(x11,x11) % 0.53/0.67 [2]E(x22,x21)+~E(x21,x22) % 0.53/0.67 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.53/0.67 [4]~E(x41,x42)+E(f2(x41,x43,x44),f2(x42,x43,x44)) % 0.53/0.67 [5]~E(x51,x52)+E(f2(x53,x51,x54),f2(x53,x52,x54)) % 0.53/0.67 [6]~E(x61,x62)+E(f2(x63,x64,x61),f2(x63,x64,x62)) % 0.53/0.67 [7]~E(x71,x72)+E(f34(x71),f34(x72)) % 0.53/0.67 [8]~P1(x81)+P1(x82)+~E(x81,x82) % 0.53/0.67 [9]P6(x92,x93)+~E(x91,x92)+~P6(x91,x93) % 0.53/0.67 [10]P6(x103,x102)+~E(x101,x102)+~P6(x103,x101) % 0.53/0.67 [11]~P2(x111)+P2(x112)+~E(x111,x112) % 0.53/0.67 [12]~P5(x121)+P5(x122)+~E(x121,x122) % 0.53/0.67 [13]~P4(x131)+P4(x132)+~E(x131,x132) % 0.53/0.67 [14]~P3(x141)+P3(x142)+~E(x141,x142) % 0.53/0.67 [15]P7(x152,x153)+~E(x151,x152)+~P7(x151,x153) % 0.53/0.67 [16]P7(x163,x162)+~E(x161,x162)+~P7(x163,x161) % 0.53/0.67 % 0.53/0.67 %------------------------------------------- % 0.53/0.67 cnf(190,plain, % 0.53/0.67 ($false), % 0.53/0.67 inference(scs_inference,[],[17,22,23,21,20,19,24,18,25,178]), % 0.53/0.67 ['proof']). % 0.53/0.67 % SZS output end Proof % 0.53/0.67 % Total time :0.010000s %------------------------------------------------------------------------------