%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : PUZ039-10 : TPTP v9.0.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n008.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 : Tue Jul 15 07:39:20 AM UTC 2025
% Result : Unsatisfiable 20.47s 20.11s
% Output : CNFRefutation 20.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 9
% Syntax : Number of formulae : 23 ( 22 unt; 0 def)
% Number of atoms : 25 ( 24 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 5 ( 3 ~; 0 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 4 con; 0-12 aty)
% Number of variables : 110 ( 23 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
state(B,V1,V2,V3,v4(s(s(o)),s(s(o))),H,S1,S2,S3,S4,E1,E2) != true,
file('theBenchmark.p',goal_state) ).
fof(e,plain,
! [B,E1,E2,H,S1,S2,S3,S4,V1,V2,V3] :
( true0 != false
& eq(B,B) = true0
& eq(state(B,V1,V2,V3,v4(s(s(o)),s(s(o))),H,S1,S2,S3,S4,E1,E2),true) = false ),
inference(encode_existential,[status(esa)],[g0]) ).
cnf(g1,plain,
true0 != false,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c1,plain,
eq(X,X) = true0,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c2,axiom,
ifeq(X,X,Y,Z) = Y,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c3,plain,
eq(state(X,Y,Z,W,v4(s(s(o)),s(s(o))),V,U,U2,U3,U4,U5,U6),true) = false,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c4,axiom,
ifeq(state(X,Y,Z,W,V,U,U2,U3,U4,U5,e1(U6,U7),e2(U8,U9)),true,state(X,Y,Z,W,V,U,U2,U3,U4,U5,e1(U8,U9),e2(U6,U7)),true) = true,
file('theBenchmark.p',swap_blanks) ).
cnf(c11,axiom,
ifeq(state(X,Y,Z,W,V,U,U2,s2(U3,U4),U5,U6,e1(s(U3),U4),U7),true,state(X,Y,Z,W,V,U,U2,s2(s(U3),U4),U5,U6,e1(U3,U4),U7),true) = true,
file('theBenchmark.p',s2_down) ).
cnf(c19,axiom,
ifeq(state(X,Y,Z,W,V,U,U2,U3,U4,s4(U5,U6),e1(U5,s(U6)),U7),true,state(X,Y,Z,W,V,U,U2,U3,U4,s4(U5,s(U6)),e1(U5,U6),U7),true) = true,
file('theBenchmark.p',s4_right) ).
cnf(c26,axiom,
ifeq(state(X,Y,Z,v3(W,V),U,U2,U3,U4,U5,U6,e1(s(s(W)),V),U7),true,state(X,Y,Z,v3(s(W),V),U,U2,U3,U4,U5,U6,e1(W,V),U7),true) = true,
file('theBenchmark.p',v3_down) ).
cnf(c30,axiom,
ifeq(state(X,Y,Z,W,V,h(U,s(U2)),U3,U4,U5,U6,e1(U,U2),U7),true,state(X,Y,Z,W,V,h(U,U2),U3,U4,U5,U6,e1(U,s(s(U2))),U7),true) = true,
file('theBenchmark.p',h_left) ).
cnf(c33,axiom,
ifeq(state(X,Y,Z,W,v4(V,s(U)),U2,U3,U4,U5,U6,e1(V,U),e2(s(V),U)),true,state(X,Y,Z,W,v4(V,U),U2,U3,U4,U5,U6,e1(V,s(U)),e2(s(V),s(U))),true) = true,
file('theBenchmark.p',v4_left) ).
cnf(c45,axiom,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),o),e2(s(s(s(s(o)))),s(s(s(o))))) = true,
file('theBenchmark.p',initial_state) ).
cnf(c46,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),o),e2(s(s(s(s(o)))),s(s(s(o))))) = true,
inference(equational,[status(thm)],[c2,c26,c45]) ).
cnf(c59,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),s(s(s(o)))),e2(s(s(o)),o)) = true,
inference(equational,[status(thm)],[c2,c4,c46]) ).
cnf(c84,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(s(s(o)))),s(s(o))),e2(s(s(o)),o)) = true,
inference(equational,[status(thm)],[c2,c19,c59]) ).
cnf(c112,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(s(o))),s(s(o))),e2(s(s(o)),o)) = true,
inference(equational,[status(thm)],[c2,c11,c84]) ).
cnf(c174,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(o)),o),e2(s(s(s(o))),s(s(o)))) = true,
inference(equational,[status(thm)],[c2,c4,c112]) ).
cnf(c579,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(o))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(o)),s(s(o))),e2(s(s(s(o))),s(s(o)))) = true,
inference(equational,[status(thm)],[c2,c30,c174]) ).
cnf(c1628,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(o))),h(s(s(o)),o),s1(s(s(s(o))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(o)),s(s(s(o)))),e2(s(s(s(o))),s(s(s(o))))) = true,
inference(equational,[status(thm)],[c2,c33,c579]) ).
cnf(c1629,plain,
true0 = false,
inference(equational,[status(thm)],[c1,c3,c1628]) ).
cnf(g2,plain,
true0 = false,
inference(equational,[status(thm)],[c1629]) ).
cnf(g3,plain,
$false,
inference(resolution,[status(thm)],[g1,g2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : PUZ039-10 : TPTP v9.0.0. Released v7.5.0.
% 0.03/0.11 % Command : run_Leo-III %s %d THM
% 0.13/0.32 % Computer : n008.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Mon Jul 14 15:56:04 EDT 2025
% 0.13/0.33 % CPUTime :
% 20.47/20.11 % SZS status Unsatisfiable
% 20.47/20.11 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------