%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : PUZ039-10 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n023.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 : 600s
% DateTime : Mon Jul 18 18:27:22 EDT 2022
% Result : Unsatisfiable 5.88s 6.05s
% Output : Refutation 5.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 9
% Syntax : Number of clauses : 24 ( 24 unt; 0 nHn; 24 RR)
% Number of literals : 24 ( 0 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 16 con; 0-12 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(ifeq(u,u,v,w),v),
file('PUZ039-10.p',unknown),
[] ).
cnf(8,axiom,
equal(ifeq(state(u,v,w,x,y,z,x1,s2(x2,x3),x4,x5,e1(s(x2),x3),x6),true__dfg,state(u,v,w,x,y,z,x1,s2(s(x2),x3),x4,x5,e1(x2,x3),x6),true__dfg),true__dfg),
file('PUZ039-10.p',unknown),
[] ).
cnf(14,axiom,
equal(ifeq(state(u,v,w,x,y,z,x1,x2,x3,s4(x4,x5),e1(x4,s(x5)),x6),true__dfg,state(u,v,w,x,y,z,x1,x2,x3,s4(x4,s(x5)),e1(x4,x5),x6),true__dfg),true__dfg),
file('PUZ039-10.p',unknown),
[] ).
cnf(28,axiom,
equal(ifeq(state(u,v,w,v3(x,y),z,x1,x2,x3,x4,x5,e1(s(s(x)),y),x6),true__dfg,state(u,v,w,v3(s(x),y),z,x1,x2,x3,x4,x5,e1(x,y),x6),true__dfg),true__dfg),
file('PUZ039-10.p',unknown),
[] ).
cnf(31,axiom,
equal(ifeq(state(u,v,w,x,v4(y,s(z)),x1,x2,x3,x4,x5,e1(y,z),e2(s(y),z)),true__dfg,state(u,v,w,x,v4(y,z),x1,x2,x3,x4,x5,e1(y,s(z)),e2(s(y),s(z))),true__dfg),true__dfg),
file('PUZ039-10.p',unknown),
[] ).
cnf(35,axiom,
equal(ifeq(state(u,v,w,x,y,h(z,s(x1)),x2,x3,x4,x5,e1(z,x1),x6),true__dfg,state(u,v,w,x,y,h(z,x1),x2,x3,x4,x5,e1(z,s(s(x1))),x6),true__dfg),true__dfg),
file('PUZ039-10.p',unknown),
[] ).
cnf(42,axiom,
equal(ifeq(state(u,v,w,x,y,z,x1,x2,x3,x4,e1(x5,x6),e2(x7,x8)),true__dfg,state(u,v,w,x,y,z,x1,x2,x3,x4,e1(x7,x8),e2(x5,x6)),true__dfg),true__dfg),
file('PUZ039-10.p',unknown),
[] ).
cnf(43,axiom,
equal(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__dfg),
file('PUZ039-10.p',unknown),
[] ).
cnf(44,axiom,
~ equal(state(u,v,w,x,v4(s(s(o)),s(s(o))),y,z,x1,x2,x3,x4,x5),true__dfg),
file('PUZ039-10.p',unknown),
[] ).
cnf(92,plain,
equal(ifeq(true__dfg,true__dfg,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__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[43,28]),
[iquote('0:SpR:43.0,28.0')] ).
cnf(94,plain,
equal(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__dfg),
inference(rew,[status(thm),theory(equality)],[1,92]),
[iquote('0:Rew:1.0,92.0')] ).
cnf(101,plain,
equal(ifeq(true__dfg,true__dfg,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__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[94,42]),
[iquote('0:SpR:94.0,42.0')] ).
cnf(111,plain,
equal(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__dfg),
inference(rew,[status(thm),theory(equality)],[1,101]),
[iquote('0:Rew:1.0,101.0')] ).
cnf(294,plain,
equal(ifeq(true__dfg,true__dfg,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__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[111,14]),
[iquote('0:SpR:111.0,14.0')] ).
cnf(300,plain,
equal(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__dfg),
inference(rew,[status(thm),theory(equality)],[1,294]),
[iquote('0:Rew:1.0,294.0')] ).
cnf(932,plain,
equal(ifeq(true__dfg,true__dfg,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__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[300,8]),
[iquote('0:SpR:300.0,8.0')] ).
cnf(942,plain,
equal(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__dfg),
inference(rew,[status(thm),theory(equality)],[1,932]),
[iquote('0:Rew:1.0,932.0')] ).
cnf(2132,plain,
equal(ifeq(true__dfg,true__dfg,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__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[942,42]),
[iquote('0:SpR:942.0,42.0')] ).
cnf(2142,plain,
equal(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__dfg),
inference(rew,[status(thm),theory(equality)],[1,2132]),
[iquote('0:Rew:1.0,2132.0')] ).
cnf(4378,plain,
equal(ifeq(true__dfg,true__dfg,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__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[2142,35]),
[iquote('0:SpR:2142.0,35.0')] ).
cnf(4391,plain,
equal(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__dfg),
inference(rew,[status(thm),theory(equality)],[1,4378]),
[iquote('0:Rew:1.0,4378.0')] ).
cnf(8034,plain,
equal(ifeq(true__dfg,true__dfg,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__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[4391,31]),
[iquote('0:SpR:4391.0,31.0')] ).
cnf(8041,plain,
equal(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__dfg),
inference(rew,[status(thm),theory(equality)],[1,8034]),
[iquote('0:Rew:1.0,8034.0')] ).
cnf(8042,plain,
$false,
inference(mrr,[status(thm)],[8041,44]),
[iquote('0:MRR:8041.0,44.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PUZ039-10 : TPTP v8.1.0. Released v7.5.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n023.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 : 600
% 0.12/0.33 % DateTime : Sun May 29 00:54:12 EDT 2022
% 0.12/0.34 % CPUTime :
% 5.88/6.05
% 5.88/6.05 SPASS V 3.9
% 5.88/6.05 SPASS beiseite: Proof found.
% 5.88/6.05 % SZS status Theorem
% 5.88/6.05 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.88/6.05 SPASS derived 4712 clauses, backtracked 0 clauses, performed 0 splits and kept 1277 clauses.
% 5.88/6.05 SPASS allocated 71710 KBytes.
% 5.88/6.05 SPASS spent 0:00:05.62 on the problem.
% 5.88/6.05 0:00:00.04 for the input.
% 5.88/6.05 0:00:00.00 for the FLOTTER CNF translation.
% 5.88/6.05 0:00:00.60 for inferences.
% 5.88/6.05 0:00:00.00 for the backtracking.
% 5.88/6.05 0:00:04.85 for the reduction.
% 5.88/6.05
% 5.88/6.05
% 5.88/6.05 Here is a proof with depth 7, length 24 :
% 5.88/6.05 % SZS output start Refutation
% See solution above
% 5.88/6.06 Formulae used in the proof : ifeq_axiom s2_down s4_right v3_down v4_left h_left swap_blanks initial_state goal_state
% 5.88/6.06
%------------------------------------------------------------------------------