%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN084+1 : TPTP v8.2.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/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 19:04:31 EDT 2024 % Result : Theorem 62.75s 63.01s % Output : CNFRefutation 63.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN084+1 : TPTP v8.2.0. Released v2.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n021.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 : Sun Jun 23 18:39:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 62.75/62.99 %------------------------------------------- % 62.75/62.99 % File :CSE---1.7 % 62.75/62.99 % Problem :theBenchmark % 62.75/62.99 % Transform :cnf % 62.75/62.99 % Format :tptp:raw % 62.75/62.99 % Command :java -jar mcs_scs.jar %d %s % 62.75/62.99 % 62.75/62.99 % Result :Theorem 62.220000s % 62.75/62.99 % Output :CNFRefutation 62.220000s % 62.75/62.99 %------------------------------------------- % 62.75/63.01 %-------------------------------------------------------------------------- % 62.75/63.01 % File : SYN084+1 : TPTP v8.2.0. Released v2.0.0. % 62.75/63.01 % Domain : Syntactic % 62.75/63.01 % Problem : Pelletier Problem 62 % 62.75/63.01 % Version : Especial. % 62.75/63.01 % English : % 62.75/63.01 % 62.75/63.01 % Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au % 62.75/63.01 % : [Pel88] Pelletier (1988), Errata % 62.75/63.01 % : [Hah94] Haehnle (1994), Email to G. Sutcliffe % 62.75/63.01 % : [Pel95] Pelletier (1995), Email to G. Sutcliffe % 62.75/63.01 % Source : [Hah94] % 62.75/63.01 % Names : Pelletier 62 [Pel86] % 62.75/63.01 % 62.75/63.01 % Status : Theorem % 62.75/63.01 % Rating : 0.00 v5.5.0, 0.08 v5.4.0, 0.09 v5.3.0, 0.13 v5.2.0, 0.07 v5.0.0, 0.05 v4.1.0, 0.06 v4.0.1, 0.05 v3.7.0, 0.00 v2.1.0 % 62.75/63.01 % Syntax : Number of formulae : 1 ( 0 unt; 0 def) % 62.75/63.01 % Number of atoms : 10 ( 0 equ) % 62.75/63.01 % Maximal formula atoms : 10 ( 10 avg) % 62.75/63.01 % Number of connectives : 12 ( 3 ~; 4 |; 2 &) % 62.75/63.01 % ( 1 <=>; 2 =>; 0 <=; 0 <~>) % 62.75/63.01 % Maximal formula depth : 7 ( 7 avg) % 62.75/63.01 % Maximal term depth : 3 ( 2 avg) % 62.75/63.01 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty) % 62.75/63.01 % Number of functors : 2 ( 2 usr; 1 con; 0-1 aty) % 62.75/63.01 % Number of variables : 2 ( 2 !; 0 ?) % 62.75/63.01 % SPC : FOF_THM_RFO_NEQ % 62.75/63.01 % 62.75/63.01 % Comments : This problem is incorrect in [Pel86] and is 'corrected' in % 62.75/63.01 % [Pel88]. The 1988 version is broken too [Pel95]. This is the % 62.75/63.01 % correct version. % 62.75/63.01 %-------------------------------------------------------------------------- % 62.75/63.01 fof(pel62,conjecture, % 62.75/63.01 ( ! [X] : % 62.75/63.01 ( ( big_p(a) % 62.75/63.01 & ( big_p(X) % 62.75/63.01 => big_p(f(X)) ) ) % 62.75/63.01 => big_p(f(f(X))) ) % 62.75/63.01 <=> ! [X1] : % 62.75/63.01 ( ( ~ big_p(a) % 62.75/63.01 | big_p(X1) % 62.75/63.01 | big_p(f(f(X1))) ) % 62.75/63.01 & ( ~ big_p(a) % 62.75/63.01 | ~ big_p(f(X1)) % 62.75/63.01 | big_p(f(f(X1))) ) ) ) ). % 62.75/63.01 % 62.75/63.01 %-------------------------------------------------------------------------- % 62.75/63.01 %------------------------------------------- % 62.75/63.01 % Proof found % 62.75/63.01 % SZS status Theorem for theBenchmark % 62.75/63.01 % SZS output start Proof % 62.75/63.02 %ClaNum:31(EqnAxiom:0) % 62.83/63.02 %VarNum:8(SingletonVarNum:4) % 62.83/63.02 %MaxLitNum:5 % 62.83/63.02 %MaxfuncDepth:2 % 62.83/63.02 %SharedTerms:19 % 62.83/63.02 %goalClause: 1 8 16 19 20 24 25 26 27 30 31 % 62.83/63.02 %singleGoalClaCount:1 % 62.83/63.02 [1]P1(a1) % 62.83/63.02 [16]~P1(a2)+P1(f5(a4))+~P1(f5(f5(a3))) % 62.83/63.02 [24]~P1(a2)+~P1(f5(f5(a3)))+~P1(f5(f5(a4))) % 62.83/63.02 [26]P1(f5(a4))+~P1(f5(f5(a2)))+~P1(f5(f5(a3))) % 62.83/63.02 [30]~P1(f5(f5(a3)))+~P1(f5(f5(a2)))+~P1(f5(f5(a4))) % 62.83/63.02 [8]~P1(a3)+~P1(a2)+P1(f5(a3))+P1(f5(a4)) % 62.83/63.02 [19]~P1(a3)+~P1(a2)+P1(f5(a3))+~P1(f5(f5(a4))) % 62.83/63.02 [20]~P1(a3)+~P1(f5(f5(a2)))+P1(f5(a3))+P1(f5(a4)) % 62.83/63.02 [27]~P1(a3)+P1(f5(a3))+~P1(f5(f5(a2)))+~P1(f5(f5(a4))) % 62.83/63.02 [25]P1(x251)+P1(x252)+~P1(a1)+P1(f5(f5(x251)))+P1(f5(f5(x252))) % 62.83/63.02 [31]~P1(a1)+~P1(f5(x311))+~P1(f5(x312))+P1(f5(f5(x311)))+P1(f5(f5(x312))) % 62.83/63.02 %EqnAxiom % 62.83/63.02 % 62.83/63.02 %------------------------------------------- % 63.00/63.18 cnf(32,plain, % 63.00/63.18 (P1(x321)+P1(x322)+P1(f5(f5(x321)))+P1(f5(f5(x322)))), % 63.00/63.18 inference(scs_inference,[],[1,25])). % 63.00/63.18 cnf(33,plain, % 63.00/63.18 (~P1(f5(x331))+~P1(f5(x332))+P1(f5(f5(x331)))+P1(f5(f5(x332)))), % 63.00/63.18 inference(scs_inference,[],[1,31])). % 63.00/63.18 cnf(34,plain, % 63.00/63.18 (P1(f5(f5(a4)))+~P1(f5(f5(a2)))+~P1(f5(f5(a3)))), % 63.00/63.18 inference(scs_inference,[],[26,33])). % 63.00/63.18 cnf(35,plain, % 63.00/63.18 (P1(a3)+~P1(f5(f5(a2)))+~P1(f5(f5(a4)))), % 63.00/63.18 inference(scs_inference,[],[30,32])). % 63.00/63.18 cnf(36,plain, % 63.00/63.18 (P1(f5(a3))+~P1(f5(f5(a2)))+~P1(f5(f5(a4)))), % 63.00/63.18 inference(scs_inference,[],[35,27])). % 63.00/63.18 cnf(40,plain, % 63.00/63.18 (P1(a2)+P1(a3)+~P1(f5(f5(a4)))), % 63.00/63.18 inference(scs_inference,[],[35,32])). % 63.00/63.18 cnf(41,plain, % 63.00/63.18 (P1(a3)+~P1(f5(f5(a3)))+~P1(f5(f5(a4)))), % 63.00/63.18 inference(scs_inference,[],[40,24])). % 63.00/63.18 cnf(42,plain, % 63.00/63.18 (P1(a3)+~P1(f5(f5(a4)))), % 63.00/63.18 inference(scs_inference,[],[41,32])). % 63.00/63.18 cnf(43,plain, % 63.00/63.18 (~P1(a2)+P1(f5(a3))+~P1(f5(f5(a4)))), % 63.00/63.18 inference(scs_inference,[],[42,19])). % 63.00/63.18 cnf(280963,plain, % 63.00/63.18 (~P1(f5(f5(a2)))+~P1(f5(f5(a3)))), % 63.00/63.18 inference(scs_inference,[],[30,34])). % 63.00/63.18 cnf(280967,plain, % 63.00/63.18 (P1(f5(f5(a2)))+P1(f5(a3))+~P1(f5(f5(a4)))), % 63.00/63.18 inference(scs_inference,[],[43,32])). % 63.00/63.18 cnf(280970,plain, % 63.00/63.18 (~P1(f5(a4))+P1(a3)), % 63.00/63.18 inference(scs_inference,[],[42,33])). % 63.00/63.18 cnf(285048,plain, % 63.00/63.18 (~P1(f5(a3))+~P1(f5(f5(a2)))), % 63.00/63.18 inference(scs_inference,[],[280963,33])). % 63.00/63.18 cnf(285050,plain, % 63.00/63.18 (~P1(a2)+P1(a3)+~P1(f5(f5(a3)))), % 63.00/63.18 inference(scs_inference,[],[16,280970])). % 63.00/63.18 cnf(285051,plain, % 63.00/63.18 (P1(f5(f5(a2)))+P1(a3)+~P1(f5(f5(a3)))), % 63.00/63.18 inference(scs_inference,[],[285050,32])). % 63.00/63.18 cnf(285052,plain, % 63.00/63.18 (P1(a3)+~P1(f5(f5(a3)))), % 63.00/63.18 inference(scs_inference,[],[285051,280963])). % 63.00/63.18 cnf(285056,plain, % 63.00/63.18 (~P1(f5(a3))+~P1(a2)+P1(f5(a4))), % 63.00/63.18 inference(scs_inference,[],[16,33])). % 63.00/63.18 cnf(285060,plain, % 63.00/63.18 (P1(f5(f5(a2)))+~P1(f5(a3))+P1(f5(a4))), % 63.00/63.18 inference(scs_inference,[],[285056,32])). % 63.00/63.18 cnf(285065,plain, % 63.00/63.18 (~P1(f5(a4))+~P1(a2)+P1(f5(a3))), % 63.00/63.18 inference(scs_inference,[],[43,33])). % 63.00/63.18 cnf(285082,plain, % 63.00/63.18 (P1(f5(f5(a2)))+~P1(f5(f5(a3)))+~P1(f5(f5(a4)))), % 63.00/63.18 inference(scs_inference,[],[24,32])). % 63.00/63.18 cnf(285083,plain, % 63.00/63.18 (~P1(f5(f5(a4)))+~P1(f5(f5(a3)))), % 63.00/63.18 inference(scs_inference,[],[285082,280963])). % 63.00/63.18 cnf(285084,plain, % 63.00/63.18 (~P1(f5(a4))+~P1(f5(f5(a3)))), % 63.00/63.18 inference(scs_inference,[],[285083,33])). % 63.00/63.18 cnf(285086,plain, % 63.00/63.18 (~P1(f5(a3))+~P1(f5(a4))), % 63.00/63.18 inference(scs_inference,[],[285084,33])). % 63.00/63.18 cnf(290070,plain, % 63.00/63.18 (~P1(f5(a3))+P1(f5(a4))), % 63.00/63.18 inference(scs_inference,[],[285060,285048])). % 63.00/63.18 cnf(290074,plain, % 63.00/63.18 (~P1(f5(a3))), % 63.00/63.18 inference(scs_inference,[],[290070,285086])). % 63.00/63.18 cnf(290075,plain, % 63.00/63.18 (~P1(a3)+~P1(a2)+P1(f5(a4))), % 63.00/63.18 inference(scs_inference,[],[290074,8])). % 63.00/63.18 cnf(290076,plain, % 63.00/63.18 (~P1(a3)+P1(f5(a4))+~P1(f5(f5(a2)))), % 63.00/63.18 inference(scs_inference,[],[290074,20])). % 63.00/63.18 cnf(290077,plain, % 63.00/63.18 (~P1(f5(f5(a2)))+~P1(f5(f5(a4)))), % 63.00/63.18 inference(scs_inference,[],[290074,36])). % 63.00/63.18 cnf(290079,plain, % 63.00/63.18 (P1(f5(f5(a2)))+~P1(f5(f5(a4)))), % 63.00/63.18 inference(scs_inference,[],[290074,280967])). % 63.00/63.18 cnf(290080,plain, % 63.00/63.18 (~P1(f5(a4))+~P1(a2)), % 63.00/63.18 inference(scs_inference,[],[290074,285065])). % 63.00/63.18 cnf(290085,plain, % 63.00/63.18 (~P1(a2)+~P1(a3)), % 63.00/63.18 inference(scs_inference,[],[290080,290075])). % 63.00/63.18 cnf(290086,plain, % 63.00/63.18 (~P1(a2)+~P1(f5(f5(a3)))), % 63.00/63.18 inference(scs_inference,[],[290085,285052])). % 63.00/63.18 cnf(290087,plain, % 63.00/63.18 (P1(f5(f5(a2)))+~P1(f5(f5(a3)))), % 63.00/63.18 inference(scs_inference,[],[290086,32])). % 63.00/63.18 cnf(290092,plain, % 63.00/63.18 (~P1(f5(f5(a4)))), % 63.00/63.18 inference(scs_inference,[],[290079,290077])). % 63.00/63.18 cnf(290093,plain, % 63.00/63.18 (~P1(f5(a4))), % 63.00/63.18 inference(scs_inference,[],[290092,33])). % 63.00/63.18 cnf(290096,plain, % 63.00/63.18 (~P1(a3)+~P1(f5(f5(a2)))), % 63.00/63.18 inference(scs_inference,[],[290093,290076])). % 63.00/63.18 cnf(290097,plain, % 63.00/63.18 (P1(f5(f5(a3)))+~P1(f5(f5(a2)))), % 63.00/63.18 inference(scs_inference,[],[290096,32])). % 63.00/63.18 cnf(290098,plain, % 63.00/63.18 (~P1(f5(f5(a3)))), % 63.00/63.18 inference(scs_inference,[],[290087,280963])). % 63.00/63.18 cnf(290099,plain, % 63.00/63.18 (~P1(f5(f5(a2)))), % 63.00/63.18 inference(scs_inference,[],[290098,290097])). % 63.00/63.18 cnf(290100,plain, % 63.00/63.18 (~P1(a3)), % 63.00/63.18 inference(scs_inference,[],[290099,290085,32])). % 63.00/63.18 cnf(290104,plain, % 63.00/63.18 ($false), % 63.00/63.18 inference(scs_inference,[],[290100,290098,32]), % 63.00/63.18 ['proof']). % 63.09/63.31 % SZS output end Proof % 63.09/63.31 % Total time :62.220000s %------------------------------------------------------------------------------