%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SYN986+1.003 : TPTP v8.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n024.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:07:30 EDT 2024
% Result : Theorem 241.99s 242.88s
% Output : CNFRefutation 243.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SYN986+1.003 : TPTP v8.2.0. Released v4.0.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n024.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 19:27:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.52/0.57 start to proof:theBenchmark
% 241.99/242.81 %-------------------------------------------
% 241.99/242.81 % File :CSE---1.7
% 241.99/242.81 % Problem :theBenchmark
% 241.99/242.81 % Transform :cnf
% 241.99/242.81 % Format :tptp:raw
% 241.99/242.81 % Command :java -jar mcs_scs.jar %d %s
% 241.99/242.81
% 241.99/242.81 % Result :Theorem 241.310000s
% 241.99/242.81 % Output :CNFRefutation 241.310000s
% 241.99/242.81 %-------------------------------------------
% 241.99/242.88 %------------------------------------------------------------------------------
% 241.99/242.88 % File : SYN986+1.003 : TPTP v8.2.0. Released v4.0.0.
% 241.99/242.88 % Domain : Syntactic
% 241.99/242.88 % Problem : Orevkov formula - size 3
% 241.99/242.88 % Version : [TS00] axioms : Especial.
% 241.99/242.88 % English : hyp(2,k,1) is defined. Each Ck has a non-normal natural deduction
% 241.99/242.88 % of size linear in k, and each normal deduction of Ck has at least
% 241.99/242.88 % hyp(2,k,1)=2_k nodes.
% 241.99/242.88
% 241.99/242.88 % Refs : [TS00] Troelstra & Schwichtenberg (2000), Basic Proof Theory
% 241.99/242.88 % : [Rat08] Raths (2008), Email to G. Sutcliffe
% 241.99/242.88 % Source : [Rat08]
% 241.99/242.88 % Names :
% 241.99/242.88
% 241.99/242.88 % Status : Theorem
% 241.99/242.88 % Rating : 0.00 v7.5.0, 0.14 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.14 v6.4.0, 0.07 v6.3.0, 0.08 v6.2.0, 0.18 v6.1.0, 0.16 v6.0.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.09 v5.3.0, 0.17 v5.2.0, 0.14 v5.1.0, 0.21 v5.0.0, 0.20 v4.1.0, 0.22 v4.0.1, 0.47 v4.0.0
% 241.99/242.88 % Syntax : Number of formulae : 3 ( 1 unt; 0 def)
% 241.99/242.88 % Number of atoms : 8 ( 0 equ)
% 241.99/242.88 % Maximal formula atoms : 4 ( 2 avg)
% 241.99/242.88 % Number of connectives : 5 ( 0 ~; 0 |; 3 &)
% 241.99/242.88 % ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% 241.99/242.88 % Maximal formula depth : 8 ( 6 avg)
% 241.99/242.88 % Maximal term depth : 2 ( 1 avg)
% 241.99/242.88 % Number of predicates : 1 ( 1 usr; 0 prp; 3-3 aty)
% 241.99/242.88 % Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% 241.99/242.88 % Number of variables : 9 ( 5 !; 4 ?)
% 241.99/242.88 % SPC : FOF_THM_RFO_NEQ
% 241.99/242.88
% 241.99/242.88 % Comments : Inspiration by Wolfgang Bibel, Helmut Schwichtenberg.
% 241.99/242.88 % : The complexity of proof seach is hyper-exponential with the size
% 241.99/242.88 % of the formulae: 2^0=1, 2^1=2, 2^2=4, 2^4=16, 2^16=65536,
% 241.99/242.88 % 2^65536 = mmmh... ?
% 241.99/242.88 %------------------------------------------------------------------------------
% 241.99/242.88 %----Include Orevkov formula
% 241.99/242.88 include('Axioms/SYN002+0.ax').
% 241.99/242.88 %------------------------------------------------------------------------------
% 241.99/242.88 fof(ck,conjecture,
% 241.99/242.88 ? [Z3,Z2,Z1,Z0] :
% 241.99/242.88 ( r(zero,zero,Z3)
% 241.99/242.88 & r(zero,Z3,Z2)
% 241.99/242.88 & r(zero,Z2,Z1)
% 241.99/242.88 & r(zero,Z1,Z0) ) ).
% 241.99/242.88
% 241.99/242.88 %------------------------------------------------------------------------------
% 241.99/242.88 %-------------------------------------------
% 241.99/242.88 % Proof found
% 241.99/242.88 % SZS status Theorem for theBenchmark
% 241.99/242.88 % SZS output start Proof
% 242.09/242.95 %ClaNum:3(EqnAxiom:0)
% 242.09/242.95 %VarNum:18(SingletonVarNum:9)
% 242.09/242.95 %MaxLitNum:4
% 242.09/242.95 %MaxfuncDepth:1
% 242.09/242.95 %SharedTerms:1
% 242.09/242.95 %goalClause: 3
% 242.09/242.95 [1]P1(x11,a1,f2(x11))
% 242.09/242.95 [2]~P1(x21,x22,x24)+~P1(x24,x22,x23)+P1(x21,f2(x22),x23)
% 242.09/242.95 [3]~P1(a1,x31,x32)+~P1(a1,x33,x31)+~P1(a1,x34,x33)+~P1(a1,a1,x34)
% 242.09/242.95 %EqnAxiom
% 242.09/242.95
% 242.09/242.95 %-------------------------------------------
% 242.73/243.56 cnf(115026,plain,
% 242.73/243.56 (~P1(x1150261,a1,x1150262)+P1(x1150261,f2(a1),f2(x1150262))),
% 242.73/243.56 inference(scs_inference,[],[1,2])).
% 242.73/243.56 cnf(205205,plain,
% 242.73/243.56 (P1(x2052051,f2(a1),f2(f2(x2052051)))),
% 242.73/243.56 inference(scs_inference,[],[1,115026])).
% 242.73/243.56 cnf(205216,plain,
% 242.73/243.56 (~P1(a1,f2(a1),a1)),
% 242.73/243.56 inference(scs_inference,[],[1,115026,3])).
% 242.73/243.56 cnf(205220,plain,
% 242.73/243.56 (~P1(a1,f2(f2(a1)),f2(a1))),
% 242.73/243.56 inference(scs_inference,[],[1,115026,3])).
% 242.73/243.56 cnf(205252,plain,
% 242.73/243.56 (~P1(f2(f2(a1)),f2(a1),f2(a1))),
% 242.73/243.56 inference(scs_inference,[],[205220,205205,2])).
% 242.73/243.56 cnf(885372,plain,
% 242.73/243.56 (P1(x8853721,a1,f2(x8853721))),
% 242.73/243.56 inference(rename_variables,[],[1])).
% 242.73/243.56 cnf(885374,plain,
% 242.73/243.56 (~P1(a1,f2(f2(a1)),x8853741)+~P1(a1,f2(a1),f2(a1))),
% 242.73/243.56 inference(scs_inference,[],[1,885372,205216,205205,2,3])).
% 242.73/243.56 cnf(886437,plain,
% 242.73/243.56 (~P1(x8864371,x8864372,x8864373)+P1(x8864374,f2(x8864372),x8864373)+~P1(x8864374,x8864372,x8864371)),
% 242.73/243.56 inference(rename_variables,[],[2])).
% 242.73/243.56 cnf(886438,plain,
% 242.73/243.56 (~P1(x8864381,f2(a1),x8864382)+P1(x8864381,f2(f2(a1)),f2(f2(x8864382)))),
% 242.73/243.56 inference(scs_inference,[],[205205,205252,1,2,886437])).
% 242.73/243.56 cnf(886444,plain,
% 242.73/243.56 (~P1(a1,f2(a1),f2(a1))),
% 242.73/243.56 inference(scs_inference,[],[205205,886438,885374])).
% 242.73/243.56 cnf(886445,plain,
% 242.73/243.56 (P1(x8864451,f2(f2(a1)),f2(f2(f2(f2(x8864451)))))),
% 242.73/243.56 inference(scs_inference,[],[205205,886438])).
% 242.73/243.56 cnf(886457,plain,
% 242.73/243.56 (P1(x8864571,a1,f2(x8864571))),
% 242.73/243.56 inference(rename_variables,[],[1])).
% 242.73/243.56 cnf(886459,plain,
% 242.73/243.56 (~P1(a1,f2(f2(f2(f2(a1)))),x8864591)),
% 242.73/243.56 inference(scs_inference,[],[205205,886445,886444,1,886457,2,3])).
% 242.73/243.56 cnf(886647,plain,
% 242.73/243.56 (~P1(x8866471,x8866472,x8866473)+P1(x8866474,f2(x8866472),x8866473)+~P1(x8866474,x8866472,x8866471)),
% 242.73/243.56 inference(rename_variables,[],[2])).
% 242.73/243.56 cnf(886648,plain,
% 242.73/243.56 (~P1(x8866481,f2(f2(a1)),x8866482)+P1(x8866481,f2(f2(f2(a1))),f2(f2(f2(f2(x8866482)))))),
% 242.73/243.56 inference(scs_inference,[],[886445,886444,1,2,886647])).
% 242.73/243.56 cnf(886658,plain,
% 242.73/243.56 (~P1(a1,f2(f2(f2(a1))),x8866581)),
% 242.73/243.56 inference(scs_inference,[],[886445,886459,886648,2])).
% 242.73/243.56 cnf(886659,plain,
% 242.73/243.56 ($false),
% 242.73/243.56 inference(scs_inference,[],[886445,886658,886648]),
% 242.73/243.56 ['proof']).
% 243.33/244.13 % SZS output end Proof
% 243.33/244.13 % Total time :241.310000s
%------------------------------------------------------------------------------