%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV001-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.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 16:45:26 EDT 2024 % Result : Unsatisfiable 58.57s 58.65s % Output : CNFRefutation 59.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV001-1 : TPTP v8.2.0. Released v1.0.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n022.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 15:21:23 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 58.57/58.62 %------------------------------------------- % 58.57/58.62 % File :CSE---1.7 % 58.57/58.62 % Problem :theBenchmark % 58.57/58.62 % Transform :cnf % 58.57/58.62 % Format :tptp:raw % 58.57/58.62 % Command :java -jar mcs_scs.jar %d %s % 58.57/58.62 % 58.57/58.62 % Result :Theorem 58.000000s % 58.57/58.62 % Output :CNFRefutation 58.000000s % 58.57/58.62 %------------------------------------------- % 58.57/58.64 %-------------------------------------------------------------------------- % 58.57/58.64 % File : SWV001-1 : TPTP v8.2.0. Released v1.0.0. % 58.57/58.64 % Domain : Software Verification % 58.57/58.64 % Problem : PV1 % 58.57/58.64 % Version : Especial. % 58.57/58.64 % English : These "clauses arose in a natural manner from work done in % 58.57/58.64 % program verification" [MOW76] p.779. % 58.57/58.64 % 58.57/58.64 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a % 58.57/58.64 % Source : [MOW76] % 58.57/58.64 % Names : PV1 [MOW76] % 58.57/58.64 % 58.57/58.64 % Status : Unsatisfiable % 58.57/58.64 % Rating : 0.00 v2.0.0 % 58.57/58.64 % Syntax : Number of clauses : 14 ( 2 unt; 2 nHn; 12 RR) % 58.57/58.64 % Number of literals : 36 ( 0 equ; 22 neg) % 58.57/58.64 % Maximal clause size : 4 ( 2 avg) % 58.57/58.64 % Maximal term depth : 1 ( 1 avg) % 58.57/58.64 % Number of predicates : 6 ( 6 usr; 0 prp; 2-3 aty) % 58.57/58.64 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 58.57/58.64 % Number of variables : 30 ( 2 sgn) % 58.57/58.64 % SPC : CNF_UNS_EPR_NEQ_NHN % 58.57/58.64 % 58.57/58.64 % Comments : This problem was contributed to [MOW76] by E. McCharen. The % 58.57/58.64 % axioms are incomplete. % 58.57/58.64 %-------------------------------------------------------------------------- % 58.57/58.64 cnf(less_or_equal_substitution1,axiom, % 58.57/58.64 ( ~ equalish(X,Y) % 58.57/58.64 | ~ less_or_equalish(X,Z) % 58.57/58.64 | less_or_equalish(Y,Z) ) ). % 58.57/58.64 % 58.57/58.64 cnf(less_or_equal_substitution2,axiom, % 58.57/58.64 ( ~ equalish(X,Y) % 58.57/58.64 | ~ less_or_equalish(Z,X) % 58.57/58.64 | less_or_equalish(Z,Y) ) ). % 58.57/58.64 % 58.57/58.64 cnf(clause_1,axiom, % 58.57/58.64 ( ~ q1(X,Y,Z) % 58.57/58.64 | ~ less_or_equalish(X,Y) % 58.57/58.64 | q2(X,Y,Z) ) ). % 58.57/58.64 % 58.57/58.64 cnf(clause_2,axiom, % 58.57/58.64 ( ~ q1(X,Y,Z) % 58.57/58.65 | less_or_equalish(X,Y) % 58.57/58.65 | q3(X,Y,Z) ) ). % 58.57/58.65 % 58.57/58.65 cnf(clause_3,axiom, % 58.57/58.65 ( ~ q2(X,Y,Z) % 58.57/58.65 | q4(X,Y,Y) ) ). % 58.57/58.65 % 58.57/58.65 cnf(clause_4,axiom, % 58.57/58.65 ( ~ q3(X,Y,Z) % 58.57/58.65 | q4(X,Y,X) ) ). % 58.57/58.65 % 58.57/58.65 cnf(less_or_equal_reflexivity,axiom, % 58.57/58.65 less_or_equalish(X,X) ). % 58.57/58.65 % 58.57/58.65 cnf(less_or_equal_implies_equal,axiom, % 58.57/58.65 ( ~ less_or_equalish(X,Y) % 58.57/58.65 | ~ less_or_equalish(Y,X) % 58.57/58.65 | equalish(X,Y) ) ). % 58.57/58.65 % 58.57/58.65 cnf(transitivity_of_less_or_equal,axiom, % 58.57/58.65 ( ~ less_or_equalish(X,Y) % 58.57/58.65 | ~ less_or_equalish(Y,Z) % 58.57/58.65 | less_or_equalish(X,Z) ) ). % 58.57/58.65 % 58.57/58.65 cnf(all_less_or_equal,axiom, % 58.57/58.65 ( less_or_equalish(X,Y) % 58.57/58.65 | less_or_equalish(Y,X) ) ). % 58.57/58.65 % 58.57/58.65 cnf(equal_implies_less_or_equal,axiom, % 58.57/58.65 ( less_or_equalish(X,Y) % 58.57/58.65 | ~ equalish(X,Y) ) ). % 58.57/58.65 % 58.57/58.65 cnf(clause_5,negated_conjecture, % 58.57/58.65 q1(a,b,c) ). % 58.57/58.65 % 58.57/58.65 cnf(clause_6,negated_conjecture, % 58.57/58.65 ( ~ q4(a,b,W) % 58.57/58.65 | ~ less_or_equalish(a,W) % 58.57/58.65 | ~ less_or_equalish(b,W) % 58.57/58.65 | ~ less_or_equalish(W,a) ) ). % 58.57/58.65 % 58.57/58.65 cnf(clause_7,negated_conjecture, % 58.57/58.65 ( ~ q4(a,b,W) % 58.57/58.65 | ~ less_or_equalish(a,W) % 58.57/58.65 | ~ less_or_equalish(b,W) % 58.57/58.65 | ~ less_or_equalish(W,b) ) ). % 58.57/58.65 % 58.57/58.65 %-------------------------------------------------------------------------- % 58.57/58.65 %------------------------------------------- % 58.57/58.65 % Proof found % 58.57/58.65 % SZS status Theorem for theBenchmark % 58.57/58.65 % SZS output start Proof % 58.57/58.66 %ClaNum:14(EqnAxiom:0) % 58.57/58.66 %VarNum:70(SingletonVarNum:30) % 58.57/58.66 %MaxLitNum:4 % 58.57/58.66 %MaxfuncDepth:0 % 58.57/58.66 %SharedTerms:4 % 58.57/58.66 %goalClause: 2 11 12 % 58.57/58.66 %singleGoalClaCount:1 % 58.57/58.66 [2]P3(a1,a2,a3) % 58.57/58.66 [1]P1(x11,x11) % 58.57/58.66 [3]P1(x32,x31)+P1(x31,x32) % 58.57/58.66 [4]~P2(x41,x42)+P1(x41,x42) % 58.57/58.66 [9]P4(x91,x92,x92)+~P5(x91,x92,x93) % 58.57/58.66 [10]P4(x101,x102,x101)+~P6(x101,x102,x103) % 58.57/58.66 [5]~P1(x52,x51)+~P1(x51,x52)+P2(x51,x52) % 58.57/58.66 [6]~P1(x61,x63)+P1(x61,x62)+~P2(x63,x62) % 58.57/58.66 [7]~P1(x73,x72)+P1(x71,x72)+~P2(x73,x71) % 58.57/58.66 [8]~P1(x81,x83)+P1(x81,x82)+~P1(x83,x82) % 58.57/58.66 [13]~P3(x131,x132,x133)+P1(x131,x132)+P6(x131,x132,x133) % 58.57/58.66 [14]~P1(x141,x142)+~P3(x141,x142,x143)+P5(x141,x142,x143) % 58.57/58.66 [11]~P1(a1,x111)+~P1(a2,x111)+~P1(x111,a1)+~P4(a1,a2,x111) % 58.57/58.66 [12]~P1(a1,x121)+~P1(a2,x121)+~P1(x121,a2)+~P4(a1,a2,x121) % 58.57/58.66 %EqnAxiom % 58.57/58.66 % 58.57/58.66 %------------------------------------------- % 58.84/58.95 cnf(24,plain, % 58.84/58.95 (P1(a1,a2)+~P4(a1,a2,a1)), % 58.84/58.95 inference(scs_inference,[],[1,3,11])). % 58.84/58.95 cnf(481519,plain, % 58.84/58.95 (P1(a1,a2)), % 58.84/58.95 inference(scs_inference,[],[2,13,10,24])). % 58.84/58.95 cnf(481527,plain, % 58.84/58.95 ($false), % 58.84/58.95 inference(scs_inference,[],[2,481519,1,14,12,9]), % 58.84/58.95 ['proof']). % 59.07/59.18 % SZS output end Proof % 59.07/59.18 % Total time :58.000000s %------------------------------------------------------------------------------