%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWX207-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n006.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 May 5 07:07:25 PM UTC 2026
% Result : Unsatisfiable 1.03s 1.24s
% Output : Refutation 1.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 14
% Syntax : Number of clauses : 32 ( 23 unt; 0 nHn; 32 RR)
% Number of literals : 41 ( 0 equ; 13 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(impl(btrue,u),u),
file('SWX207-1.p',unknown),
[] ).
cnf(3,axiom,
equal(append(nil,u),u),
file('SWX207-1.p',unknown),
[] ).
cnf(4,axiom,
equal(append(cons(u,v),w),cons(u,append(v,w))),
file('SWX207-1.p',unknown),
[] ).
cnf(7,axiom,
equal(cons(a,nil),linP(pA)),
file('SWX207-1.p',unknown),
[] ).
cnf(9,axiom,
equal(linP(pE),nil),
file('SWX207-1.p',unknown),
[] ).
cnf(10,axiom,
equal(append(linP(u),linP(v)),linC(c2(u,v))),
file('SWX207-1.p',unknown),
[] ).
cnf(11,axiom,
equal(impl(eq(linC(u),linC(v)),eq4(u,v)),unambig(u,v)),
file('SWX207-1.p',unknown),
[] ).
cnf(18,axiom,
equal(eq3(pE,pA),bfalse),
file('SWX207-1.p',unknown),
[] ).
cnf(38,axiom,
( ~ equal(eq3(u,v),bfalse)
| equal(eq4(c2(u,w),c2(v,x)),bfalse) ),
file('SWX207-1.p',unknown),
[] ).
cnf(40,axiom,
equal(eq(u,u),btrue),
file('SWX207-1.p',unknown),
[] ).
cnf(41,axiom,
equal(eq2(u,u),btrue),
file('SWX207-1.p',unknown),
[] ).
cnf(44,axiom,
equal(eq5(u,u),btrue),
file('SWX207-1.p',unknown),
[] ).
cnf(46,axiom,
( ~ equal(eq2(u,v),btrue)
| equal(eq(cons(u,w),cons(v,x)),eq(w,x)) ),
file('SWX207-1.p',unknown),
[] ).
cnf(49,axiom,
~ equal(eq5(unambig(u,v),bfalse),btrue),
file('SWX207-1.p',unknown),
[] ).
cnf(103,plain,
equal(append(nil,linP(u)),linC(c2(pE,u))),
inference(spr,[status(thm),theory(equality)],[9,10]),
[iquote('0:SpR:9.0,10.0')] ).
cnf(104,plain,
equal(linC(c2(pE,u)),linP(u)),
inference(rew,[status(thm),theory(equality)],[3,103]),
[iquote('0:Rew:3.0,103.0')] ).
cnf(125,plain,
equal(cons(a,append(nil,u)),append(linP(pA),u)),
inference(spr,[status(thm),theory(equality)],[7,4]),
[iquote('0:SpR:7.0,4.0')] ).
cnf(128,plain,
equal(append(linP(pA),u),cons(a,u)),
inference(rew,[status(thm),theory(equality)],[3,125]),
[iquote('0:Rew:3.0,125.0')] ).
cnf(183,plain,
equal(cons(a,linP(u)),linC(c2(pA,u))),
inference(spr,[status(thm),theory(equality)],[128,10]),
[iquote('0:SpR:128.0,10.0')] ).
cnf(228,plain,
( ~ equal(eq3(u,v),bfalse)
| equal(impl(eq(linC(c2(u,w)),linC(c2(v,x))),bfalse),unambig(c2(u,w),c2(v,x))) ),
inference(spr,[status(thm),theory(equality)],[38,11]),
[iquote('0:SpR:38.1,11.0')] ).
cnf(290,plain,
( ~ equal(eq2(a,u),btrue)
| equal(eq(linP(pA),cons(u,v)),eq(nil,v)) ),
inference(spr,[status(thm),theory(equality)],[7,46]),
[iquote('0:SpR:7.0,46.1')] ).
cnf(836,plain,
( ~ equal(eq2(a,a),btrue)
| equal(eq(linP(pA),linC(c2(pA,u))),eq(nil,linP(u))) ),
inference(spr,[status(thm),theory(equality)],[183,290]),
[iquote('0:SpR:183.0,290.1')] ).
cnf(841,plain,
( ~ equal(btrue,btrue)
| equal(eq(linP(pA),linC(c2(pA,u))),eq(nil,linP(u))) ),
inference(rew,[status(thm),theory(equality)],[41,836]),
[iquote('0:Rew:41.0,836.0')] ).
cnf(842,plain,
equal(eq(linP(pA),linC(c2(pA,u))),eq(nil,linP(u))),
inference(obv,[status(thm),theory(equality)],[841]),
[iquote('0:Obv:841.0')] ).
cnf(1178,plain,
( ~ equal(eq3(pE,u),bfalse)
| equal(impl(eq(linP(v),linC(c2(u,w))),bfalse),unambig(c2(pE,v),c2(u,w))) ),
inference(spr,[status(thm),theory(equality)],[104,228]),
[iquote('0:SpR:104.0,228.1')] ).
cnf(2689,plain,
( ~ equal(eq3(pE,pA),bfalse)
| equal(unambig(c2(pE,pA),c2(pA,u)),impl(eq(nil,linP(u)),bfalse)) ),
inference(spr,[status(thm),theory(equality)],[842,1178]),
[iquote('0:SpR:842.0,1178.1')] ).
cnf(2707,plain,
( ~ equal(bfalse,bfalse)
| equal(unambig(c2(pE,pA),c2(pA,u)),impl(eq(nil,linP(u)),bfalse)) ),
inference(rew,[status(thm),theory(equality)],[18,2689]),
[iquote('0:Rew:18.0,2689.0')] ).
cnf(2708,plain,
equal(unambig(c2(pE,pA),c2(pA,u)),impl(eq(nil,linP(u)),bfalse)),
inference(obv,[status(thm),theory(equality)],[2707]),
[iquote('0:Obv:2707.0')] ).
cnf(7409,plain,
~ equal(eq5(impl(eq(nil,linP(u)),bfalse),bfalse),btrue),
inference(spl,[status(thm),theory(equality)],[2708,49]),
[iquote('0:SpL:2708.0,49.0')] ).
cnf(7410,plain,
~ equal(eq5(impl(eq(nil,nil),bfalse),bfalse),btrue),
inference(spl,[status(thm),theory(equality)],[9,7409]),
[iquote('0:SpL:9.0,7409.0')] ).
cnf(7419,plain,
~ equal(btrue,btrue),
inference(rew,[status(thm),theory(equality)],[44,7410,1,40]),
[iquote('0:Rew:44.0,7410.0,1.0,7410.0,40.0,7410.0')] ).
cnf(7420,plain,
$false,
inference(obv,[status(thm),theory(equality)],[7419]),
[iquote('0:Obv:7419.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX207-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : run_spass %d %s
% 0.16/0.34 % Computer : n006.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 11:36:15 EDT 2026
% 0.16/0.34 % CPUTime :
% 1.03/1.24
% 1.03/1.24 SPASS V 3.9
% 1.03/1.24 SPASS beiseite: Proof found.
% 1.03/1.24 % SZS status Theorem
% 1.03/1.24 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.03/1.24 SPASS derived 5168 clauses, backtracked 0 clauses, performed 0 splits and kept 1725 clauses.
% 1.03/1.24 SPASS allocated 70170 KBytes.
% 1.03/1.24 SPASS spent 0:00:00.85 on the problem.
% 1.03/1.24 0:00:00.04 for the input.
% 1.03/1.24 0:00:00.00 for the FLOTTER CNF translation.
% 1.03/1.24 0:00:00.07 for inferences.
% 1.03/1.24 0:00:00.00 for the backtracking.
% 1.03/1.24 0:00:00.69 for the reduction.
% 1.03/1.24
% 1.03/1.24
% 1.03/1.24 Here is a proof with depth 6, length 32 :
% 1.03/1.24 % SZS output start Refutation
% See solution above
% 1.03/1.24 Formulae used in the proof : axiom axiom_002 axiom_003 axiom_006 axiom_008 axiom_009 axiom_010 axiom_017 axiom_037 axiom_039 axiom_040 axiom_043 axiom_045 goal
% 1.03/1.24
%------------------------------------------------------------------------------