%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN729-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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:06:26 EDT 2024 % Result : Unsatisfiable 58.57s 59.06s % Output : CNFRefutation 58.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SYN729-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n001.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 : Sun Jun 23 23:06:23 EDT 2024 % 0.13/0.35 % CPUTime : % 0.51/0.60 start to proof:theBenchmark % 58.57/59.04 %------------------------------------------- % 58.57/59.04 % File :CSE---1.7 % 58.57/59.04 % Problem :theBenchmark % 58.57/59.04 % Transform :cnf % 58.57/59.04 % Format :tptp:raw % 58.57/59.04 % Command :java -jar mcs_scs.jar %d %s % 58.57/59.04 % 58.57/59.04 % Result :Theorem 58.000000s % 58.57/59.04 % Output :CNFRefutation 58.000000s % 58.57/59.04 %------------------------------------------- % 58.57/59.06 %-------------------------------------------------------------------------- % 58.57/59.06 % File : SYN729-1 : TPTP v8.2.0. Released v2.5.0. % 58.57/59.06 % Domain : Syntactic % 58.57/59.06 % Problem : Peter Andrews Problem THM72 % 58.57/59.06 % Version : Especial. % 58.57/59.06 % English : % 58.57/59.06 % 58.57/59.06 % Refs : [And97] Andrews (1994), Email to G. Sutcliffe % 58.57/59.06 % Source : [And97] % 58.57/59.06 % Names : THM72 [And97] % 58.57/59.06 % 58.57/59.06 % Status : Unsatisfiable % 58.57/59.06 % Rating : 0.00 v5.3.0, 0.05 v5.2.0, 0.00 v2.5.0 % 58.57/59.06 % Syntax : Number of clauses : 6 ( 1 unt; 0 nHn; 6 RR) % 58.57/59.06 % Number of literals : 11 ( 0 equ; 6 neg) % 58.57/59.06 % Maximal clause size : 2 ( 1 avg) % 58.57/59.06 % Maximal term depth : 4 ( 1 avg) % 58.57/59.06 % Number of predicates : 2 ( 2 usr; 0 prp; 1-2 aty) % 58.57/59.06 % Number of functors : 4 ( 4 usr; 1 con; 0-1 aty) % 58.57/59.06 % Number of variables : 5 ( 0 sgn) % 58.57/59.06 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.57/59.06 % 58.57/59.06 % Comments : % 58.57/59.06 %-------------------------------------------------------------------------- % 58.57/59.06 cnf(thm72_1,negated_conjecture, % 58.57/59.06 ( l(A,g(h(sk1(A)))) % 58.57/59.06 | ~ p(A) ) ). % 58.57/59.06 % 58.57/59.06 cnf(thm72_2,negated_conjecture, % 58.57/59.06 ( p(sk1(A)) % 58.57/59.06 | ~ p(A) ) ). % 58.57/59.06 % 58.57/59.06 cnf(thm72_3,negated_conjecture, % 58.57/59.06 ( p(g(A)) % 58.57/59.06 | ~ p(A) ) ). % 58.57/59.06 % 58.57/59.06 cnf(thm72_4,negated_conjecture, % 58.57/59.06 ( p(h(A)) % 58.57/59.06 | ~ p(A) ) ). % 58.57/59.06 % 58.57/59.06 cnf(thm72_5,negated_conjecture, % 58.57/59.06 p(sk2) ). % 58.57/59.06 % 58.57/59.06 cnf(thm72_6,negated_conjecture, % 58.57/59.06 ( ~ p(A) % 58.57/59.06 | ~ l(sk2,A) ) ). % 58.57/59.06 % 58.57/59.06 %-------------------------------------------------------------------------- % 58.57/59.06 %------------------------------------------- % 58.57/59.06 % Proof found % 58.57/59.06 % SZS status Theorem for theBenchmark % 58.57/59.06 % SZS output start Proof % 58.57/59.07 %ClaNum:6(EqnAxiom:0) % 58.57/59.07 %VarNum:11(SingletonVarNum:5) % 58.57/59.07 %MaxLitNum:2 % 58.57/59.07 %MaxfuncDepth:3 % 58.57/59.07 %SharedTerms:2 % 58.57/59.07 %goalClause: 1 2 3 4 5 6 % 58.57/59.07 %singleGoalClaCount:1 % 58.57/59.07 [1]P1(a1) % 58.57/59.07 [5]~P1(x51)+~P2(a1,x51) % 58.57/59.07 [2]~P1(x21)+P1(f2(x21)) % 58.57/59.07 [3]~P1(x31)+P1(f3(x31)) % 58.57/59.07 [4]~P1(x41)+P1(f4(x41)) % 58.57/59.07 [6]~P1(x61)+P2(x61,f4(f3(f2(x61)))) % 58.57/59.07 %EqnAxiom % 58.57/59.07 % 58.57/59.07 %------------------------------------------- % 58.66/59.14 cnf(26,plain, % 58.66/59.14 (P1(f4(f2(a1)))), % 58.66/59.14 inference(scs_inference,[],[1,2,4])). % 58.66/59.14 cnf(34,plain, % 58.66/59.14 (P1(f3(f2(a1)))), % 58.66/59.14 inference(scs_inference,[],[1,2,3])). % 58.66/59.14 cnf(119511,plain, % 58.66/59.14 (~P1(f4(f3(f2(a1))))), % 58.66/59.14 inference(scs_inference,[],[1,2,3,4,6,5])). % 58.66/59.14 cnf(119567,plain, % 58.66/59.14 ($false), % 58.66/59.14 inference(scs_inference,[],[119511,34,26,2,3,4]), % 58.66/59.14 ['proof']). % 58.81/59.23 % SZS output end Proof % 58.81/59.23 % Total time :58.000000s %------------------------------------------------------------------------------