%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN009-3 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n001.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 19:04:14 EDT 2024 % Result : Unsatisfiable 0.62s 0.70s % Output : CNFRefutation 0.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : SYN009-3 : TPTP v8.2.0. Released v2.5.0. % 0.14/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.15/0.35 % Computer : n001.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Sun Jun 23 20:42:09 EDT 2024 % 0.15/0.36 % CPUTime : % 0.62/0.67 start to proof:theBenchmark % 0.62/0.70 %------------------------------------------- % 0.62/0.70 % File :CSE---1.7 % 0.62/0.70 % Problem :theBenchmark % 0.62/0.70 % Transform :cnf % 0.62/0.70 % Format :tptp:raw % 0.62/0.70 % Command :java -jar mcs_scs.jar %d %s % 0.62/0.70 % 0.62/0.70 % Result :Theorem 0.000000s % 0.62/0.70 % Output :CNFRefutation 0.000000s % 0.62/0.70 %------------------------------------------- % 0.62/0.70 %-------------------------------------------------------------------------- % 0.62/0.70 % File : SYN009-3 : TPTP v8.2.0. Released v2.5.0. % 0.62/0.70 % Domain : Syntactic % 0.62/0.70 % Problem : A problem to demonstrate the usefulness of relevancy testing % 0.62/0.70 % Version : Especial. % 0.62/0.70 % English : % 0.62/0.70 % 0.62/0.70 % Refs : [He01a] I-SATCHMO: An Improvement of SATCHMO % 0.62/0.70 % : [He01b] UNSEARCHMO: Eliminating Redundant Search Space on Back % 0.62/0.70 % Source : [He01a] % 0.62/0.70 % Names : Example 5.1 [He01a] % 0.62/0.70 % : Example 5.2 [He01] % 0.62/0.70 % 0.62/0.70 % Status : Unsatisfiable % 0.62/0.70 % Rating : 0.00 v2.5.0 % 0.62/0.70 % Syntax : Number of clauses : 10 ( 5 unt; 2 nHn; 10 RR) % 0.62/0.70 % Number of literals : 20 ( 0 equ; 11 neg) % 0.62/0.70 % Maximal clause size : 6 ( 2 avg) % 0.62/0.70 % Maximal term depth : 1 ( 1 avg) % 0.62/0.70 % Number of predicates : 7 ( 7 usr; 0 prp; 1-3 aty) % 0.62/0.70 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 0.62/0.70 % Number of variables : 18 ( 3 sgn) % 0.62/0.70 % SPC : CNF_UNS_EPR_NEQ_NHN % 0.62/0.70 % 0.62/0.70 % Comments : % 0.62/0.70 %-------------------------------------------------------------------------- % 0.62/0.70 cnf(clause_1,negated_conjecture, % 0.62/0.70 ( ~ p(X,Y,Z) % 0.62/0.70 | ~ t(X,Y,Z) ) ). % 0.62/0.70 % 0.62/0.70 cnf(clause_2,negated_conjecture, % 0.62/0.70 ( ~ q(X,Y,Z) % 0.62/0.70 | ~ t(X,Y,Z) ) ). % 0.62/0.70 % 0.62/0.70 cnf(clause_3,negated_conjecture, % 0.62/0.70 ( ~ r(X,Y,Z) % 0.62/0.70 | ~ t(X,Y,Z) ) ). % 0.62/0.70 % 0.62/0.70 cnf(clause_4,negated_conjecture, % 0.62/0.70 s(a) ). % 0.62/0.70 % 0.62/0.70 cnf(clause_5,negated_conjecture, % 0.62/0.70 s(b) ). % 0.62/0.70 % 0.62/0.70 cnf(clause_6,negated_conjecture, % 0.62/0.70 s(c) ). % 0.62/0.70 % 0.62/0.70 cnf(clause_7,negated_conjecture, % 0.62/0.70 ~ v(X,Y,Z) ). % 0.62/0.70 % 0.62/0.70 cnf(clause_8,negated_conjecture, % 0.62/0.70 u(c,c,c) ). % 0.62/0.70 % 0.62/0.70 cnf(clause_9,negated_conjecture, % 0.62/0.70 ( ~ s(X) % 0.62/0.70 | ~ s(Y) % 0.62/0.70 | ~ s(Z) % 0.62/0.70 | p(X,Y,Z) % 0.62/0.70 | q(X,Y,Z) % 0.62/0.70 | r(X,Y,Z) ) ). % 0.62/0.70 % 0.62/0.70 cnf(clause_10,negated_conjecture, % 0.62/0.70 ( ~ u(X,Y,Z) % 0.62/0.70 | t(X,Y,Z) % 0.62/0.70 | v(X,Y,Z) ) ). % 0.62/0.70 % 0.62/0.70 %-------------------------------------------------------------------------- % 0.62/0.70 %------------------------------------------- % 0.62/0.70 % Proof found % 0.62/0.70 % SZS status Theorem for theBenchmark % 0.62/0.70 % SZS output start Proof % 0.62/0.71 %ClaNum:10(EqnAxiom:0) % 0.62/0.71 %VarNum:42(SingletonVarNum:18) % 0.62/0.71 %MaxLitNum:6 % 0.62/0.71 %MaxfuncDepth:0 % 0.62/0.71 %SharedTerms:7 % 0.62/0.71 %goalClause: 1 2 3 4 5 6 7 8 9 10 % 0.62/0.71 %singleGoalClaCount:5 % 0.62/0.71 [1]P1(a1) % 0.62/0.71 [2]P1(a2) % 0.62/0.71 [3]P1(a3) % 0.62/0.71 [4]P5(a3,a3,a3) % 0.62/0.71 [5]~P7(x51,x52,x53) % 0.62/0.71 [6]~P6(x61,x62,x63)+~P2(x61,x62,x63) % 0.62/0.71 [7]~P3(x71,x72,x73)+~P6(x71,x72,x73) % 0.62/0.71 [8]~P4(x81,x82,x83)+~P6(x81,x82,x83) % 0.62/0.71 [10]P7(x101,x102,x103)+~P5(x101,x102,x103)+P6(x101,x102,x103) % 0.62/0.71 [9]P3(x91,x92,x93)+P4(x91,x92,x93)+~P1(x93)+~P1(x92)+~P1(x91)+P2(x91,x92,x93) % 0.62/0.71 %EqnAxiom % 0.62/0.71 % 0.62/0.71 %------------------------------------------- % 0.62/0.71 cnf(20,plain, % 0.62/0.71 ($false), % 0.62/0.71 inference(scs_inference,[],[5,3,4,10,7,8,9,6]), % 0.62/0.71 ['proof']). % 0.62/0.71 % SZS output end Proof % 0.62/0.71 % Total time :0.000000s %------------------------------------------------------------------------------