%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWX200+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n025.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 : Tue May 5 06:57:08 PM UTC 2026 % Result : Theorem 58.62s 58.70s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX200+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.32 % Computer : n025.cluster.edu % 0.14/0.32 % Model : x86_64 x86_64 % 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.32 % Memory : 8042.1875MB % 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.32 % CPULimit : 300 % 0.14/0.32 % WCLimit : 300 % 0.14/0.32 % DateTime : Tue May 5 11:15:28 EDT 2026 % 0.14/0.32 % CPUTime : % 0.37/0.50 start to proof:theBenchmark % 58.53/58.69 %------------------------------------------- % 58.53/58.69 % File :CSE---1.7 % 58.53/58.69 % Problem :theBenchmark % 58.53/58.69 % Transform :cnf % 58.53/58.69 % Format :tptp:raw % 58.53/58.69 % Command :java -jar mcs_scs.jar %d %s % 58.53/58.69 % 58.53/58.69 % Result :Theorem 58.120000s % 58.53/58.69 % Output :CNFRefutation 58.120000s % 58.53/58.69 %------------------------------------------- % 58.62/58.70 %------------------------------------------------------------------------------ % 58.62/58.70 % File : SWX200+1 : TPTP v9.3.0. Released v9.3.0. % 58.62/58.70 % Domain : Software Verification % 58.62/58.70 % Problem : Faulty property about merge % 58.62/58.70 % Version : Especial. % 58.62/58.70 % English : % 58.62/58.70 % 58.62/58.70 % Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe % 58.62/58.70 % Source : [CST26] % 58.62/58.70 % Names : MergeSort_prop_merge_ord_not3.p [CST26] % 58.62/58.70 % 58.62/58.70 % Status : Theorem % 58.62/58.70 % Rating : ? v9.3.0 % 58.62/58.70 % Syntax : Number of formulae : 16 ( 11 unt; 0 def) % 58.62/58.70 % Number of atoms : 23 ( 9 equ) % 58.62/58.70 % Maximal formula atoms : 3 ( 1 avg) % 58.62/58.70 % Number of connectives : 13 ( 6 ~; 0 |; 1 &) % 58.62/58.70 % ( 2 <=>; 4 =>; 0 <=; 0 <~>) % 58.62/58.70 % Maximal formula depth : 7 ( 4 avg) % 58.62/58.70 % Maximal term depth : 4 ( 1 avg) % 58.62/58.70 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty) % 58.62/58.70 % Number of functors : 8 ( 8 usr; 2 con; 0-2 aty) % 58.62/58.70 % Number of variables : 29 ( 27 !; 2 ?) % 58.62/58.70 % SPC : FOF_THM_RFO_SEQ % 58.62/58.70 % 58.62/58.70 % Comments : % 58.62/58.70 %------------------------------------------------------------------------------ % 58.62/58.70 fof(axiom_001,axiom, % 58.62/58.70 ! [X,X2] : head(cons(X,X2)) = X ). % 58.62/58.70 % 58.62/58.70 fof(axiom_002,axiom, % 58.62/58.70 ! [X,X2] : tail(cons(X,X2)) = X2 ). % 58.62/58.70 % 58.62/58.70 fof(axiom_003,axiom, % 58.62/58.70 ! [X,X2] : nil != cons(X,X2) ). % 58.62/58.70 % 58.62/58.70 fof(axiom_004,axiom, % 58.62/58.70 ! [X] : proj1S(s(X)) = X ). % 58.62/58.70 % 58.62/58.70 fof(axiom_005,axiom, % 58.62/58.70 ! [X] : z != s(X) ). % 58.62/58.70 % 58.62/58.70 fof(axiom_006,axiom, % 58.62/58.70 ! [Y] : leqNat(z,Y) ). % 58.62/58.70 % 58.62/58.70 fof(axiom_007,axiom, % 58.62/58.70 ! [Z] : ~ leqNat(s(Z),z) ). % 58.62/58.70 % 58.62/58.70 fof(axiom_008,axiom, % 58.62/58.70 ! [Z,M] : % 58.62/58.70 ( leqNat(s(Z),s(M)) % 58.62/58.70 <=> leqNat(Z,M) ) ). % 58.62/58.70 % 58.62/58.70 fof(axiom_009,axiom, % 58.62/58.70 ! [Y] : merge(nil,Y) = Y ). % 58.62/58.70 % 58.62/58.70 fof(axiom_010,axiom, % 58.62/58.70 ! [Z,Xs] : merge(cons(Z,Xs),nil) = cons(Z,Xs) ). % 58.62/58.70 % 58.62/58.70 fof(axiom_011,axiom, % 58.62/58.70 ! [Z,Xs,Y2,Ys] : % 58.62/58.70 ( leqNat(Z,Y2) % 58.62/58.70 => merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Z,merge(Xs,cons(Y2,Ys))) ) ). % 58.62/58.70 % 58.62/58.70 fof(axiom_012,axiom, % 58.62/58.70 ! [Z,Xs,Y2,Ys] : % 58.62/58.70 ( ~ leqNat(Z,Y2) % 58.62/58.70 => merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Y2,merge(cons(Z,Xs),Ys)) ) ). % 58.62/58.70 % 58.62/58.70 fof(axiom_013,axiom, % 58.62/58.70 ord(nil) ). % 58.62/58.70 % 58.62/58.70 fof(axiom_014,axiom, % 58.62/58.70 ! [Y] : ord(cons(Y,nil)) ). % 58.62/58.70 % 58.62/58.70 fof(axiom_015,axiom, % 58.62/58.70 ! [Y,Y2,Xs] : % 58.62/58.70 ( ord(cons(Y,cons(Y2,Xs))) % 58.62/58.70 <=> ( leqNat(Y,Y2) % 58.62/58.70 & ord(cons(Y2,Xs)) ) ) ). % 58.62/58.70 % 58.62/58.70 fof(goal_016,conjecture, % 58.62/58.70 ? [Xs,Ys] : % 58.62/58.70 ~ ( ord(Xs) % 58.62/58.70 => ( ~ ord(Ys) % 58.62/58.70 => ord(merge(Xs,Ys)) ) ) ). % 58.62/58.70 % 58.62/58.70 %------------------------------------------------------------------------------ % 58.62/58.70 %------------------------------------------- % 58.62/58.70 % Proof found % 58.62/58.70 % SZS status Theorem for theBenchmark % 58.62/58.70 % SZS output start Proof % 58.62/58.71 %ClaNum:33(EqnAxiom:14) % 58.62/58.71 %VarNum:69(SingletonVarNum:37) % 58.62/58.71 %MaxLitNum:3 % 58.62/58.71 %MaxfuncDepth:3 % 58.62/58.71 %SharedTerms:3 % 58.62/58.71 %goalClause: 26 % 58.62/58.71 [15]P1(a1) % 58.62/58.71 [17]P2(a7,x171) % 58.62/58.71 [18]E(f2(a1,x181),x181) % 58.62/58.71 [19]P1(f3(x191,a1)) % 58.62/58.71 [23]~E(f5(x231),a7) % 58.62/58.71 [25]~P2(f5(x251),a7) % 58.62/58.71 [16]E(f6(f5(x161)),x161) % 58.62/58.71 [24]~E(f3(x241,x242),a1) % 58.62/58.71 [20]E(f4(f3(x201,x202)),x201) % 58.62/58.71 [21]E(f8(f3(x211,x212)),x212) % 58.62/58.71 [22]E(f2(f3(x221,x222),a1),f3(x221,x222)) % 58.62/58.71 [27]~P2(x271,x272)+P2(f5(x271),f5(x272)) % 58.62/58.71 [28]P2(x281,x282)+~P2(f5(x281),f5(x282)) % 58.62/58.71 [29]P2(x291,x292)+~P1(f3(x291,f3(x292,x293))) % 58.62/58.71 [31]P1(f3(x311,x312))+~P1(f3(x313,f3(x311,x312))) % 58.62/58.71 [32]P2(x322,x321)+E(f3(x321,f2(f3(x322,x323),x324)),f2(f3(x322,x323),f3(x321,x324))) % 58.62/58.71 [33]~P2(x331,x333)+E(f3(x331,f2(x332,f3(x333,x334))),f2(f3(x331,x332),f3(x333,x334))) % 58.62/58.71 [26]~P1(x262)+P1(x261)+P1(f2(x262,x261)) % 58.62/58.71 [30]~P2(x301,x302)+~P1(f3(x302,x303))+P1(f3(x301,f3(x302,x303))) % 58.62/58.71 %EqnAxiom % 58.62/58.71 [1]E(x11,x11) % 58.62/58.71 [2]E(x22,x21)+~E(x21,x22) % 58.62/58.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.62/58.71 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 58.62/58.71 [5]~E(x51,x52)+E(f6(x51),f6(x52)) % 58.62/58.71 [6]~E(x61,x62)+E(f2(x61,x63),f2(x62,x63)) % 58.62/58.71 [7]~E(x71,x72)+E(f2(x73,x71),f2(x73,x72)) % 58.62/58.71 [8]~E(x81,x82)+E(f3(x81,x83),f3(x82,x83)) % 58.62/58.71 [9]~E(x91,x92)+E(f3(x93,x91),f3(x93,x92)) % 58.62/58.71 [10]~E(x101,x102)+E(f8(x101),f8(x102)) % 58.62/58.71 [11]~E(x111,x112)+E(f4(x111),f4(x112)) % 58.62/58.71 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 58.62/58.71 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133) % 58.62/58.71 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141) % 58.62/58.71 % 58.62/58.71 %------------------------------------------- % 58.62/58.71 cnf(100,plain, % 58.62/58.71 (~P1(f3(f5(f5(x1001)),f3(f5(a7),x1002)))), % 58.62/58.71 inference(scs_inference,[],[25,29,28])). % 58.62/58.71 cnf(101,plain, % 58.62/58.71 (~P2(f5(f5(x1011)),f5(a7))), % 58.62/58.71 inference(scs_inference,[],[100,19,30])). % 58.62/58.71 cnf(996,plain, % 58.62/58.71 (~P1(f2(a1,f3(f5(f5(x9961)),f3(f5(a7),x9962))))), % 58.62/58.71 inference(scs_inference,[],[101,18,29,12])). % 58.62/58.71 cnf(1000,plain, % 58.62/58.71 (P1(f2(a1,f3(f5(f5(x10001)),f3(f5(a7),x10002))))), % 58.62/58.71 inference(scs_inference,[],[101,15,29,26])). % 58.62/58.71 cnf(1014,plain, % 58.62/58.71 ($false), % 58.62/58.71 inference(scs_inference,[],[996,1000]), % 58.62/58.71 ['proof']). % 58.62/58.72 % SZS output end Proof % 58.62/58.72 % Total time :58.120000s %------------------------------------------------------------------------------