%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWX063+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n028.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 Apr 1 02:16:27 AM UTC 2025
% Result : Theorem 6.79s 6.97s
% Output : Refutation 6.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 16
% Syntax : Number of clauses : 52 ( 26 unt; 4 nHn; 52 RR)
% Number of literals : 82 ( 0 equ; 37 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
list_succeeds(skc4),
file('SWX063+1.p',unknown),
[] ).
cnf(4,axiom,
list_succeeds(skc296),
file('SWX063+1.p',unknown),
[] ).
cnf(18,axiom,
equal(rev(nil),nil),
file('SWX063+1.p',unknown),
[] ).
cnf(33,axiom,
~ equal(rev(rev(skc4)),skc4),
file('SWX063+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ n_reverse_succeeds(u,v)
| list_succeeds(u) ),
file('SWX063+1.p',unknown),
[] ).
cnf(68,axiom,
( ~ n_reverse_succeeds(u,v)
| list_succeeds(v) ),
file('SWX063+1.p',unknown),
[] ).
cnf(117,axiom,
( ~ list_succeeds(u)
| n_reverse_succeeds(u,skf302(u)) ),
file('SWX063+1.p',unknown),
[] ).
cnf(161,axiom,
( equal(skc295,nil)
| equal(cons(skc297,skc296),skc295) ),
file('SWX063+1.p',unknown),
[] ).
cnf(162,axiom,
( equal(skc295,nil)
| equal(rev(rev(skc296)),skc296) ),
file('SWX063+1.p',unknown),
[] ).
cnf(185,axiom,
( ~ list_succeeds(u)
| append_succeeds(u,v,skf286(v,u)) ),
file('SWX063+1.p',unknown),
[] ).
cnf(301,axiom,
( ~ list_succeeds(u)
| ~ n_reverse_succeeds(u,v)
| equal(rev(u),v) ),
file('SWX063+1.p',unknown),
[] ).
cnf(370,axiom,
( ~ list_succeeds(u)
| equal(u,nil)
| equal(cons(skf238(u),skf237(u)),u) ),
file('SWX063+1.p',unknown),
[] ).
cnf(395,axiom,
( ~ append_succeeds(u,v,w)
| ~ append_succeeds(u,x,w)
| equal(x,v) ),
file('SWX063+1.p',unknown),
[] ).
cnf(438,axiom,
( ~ list_succeeds(u)
| equal(a42__a42_(rev(u),cons(v,nil)),rev(cons(v,u))) ),
file('SWX063+1.p',unknown),
[] ).
cnf(439,axiom,
( ~ list_succeeds(u)
| equal(cons(v,rev(u)),rev(a42__a42_(u,cons(v,nil)))) ),
file('SWX063+1.p',unknown),
[] ).
cnf(440,axiom,
( ~ list_succeeds(u)
| ~ equal(rev(rev(skc295)),skc295)
| equal(rev(rev(u)),u) ),
file('SWX063+1.p',unknown),
[] ).
cnf(636,plain,
( ~ n_reverse_succeeds(u,v)
| equal(rev(u),v) ),
inference(mrr,[status(thm)],[301,67]),
[iquote('0:MRR:301.0,67.1')] ).
cnf(684,plain,
( equal(skc4,nil)
| equal(cons(skf238(skc4),skf237(skc4)),skc4) ),
inference(res,[status(thm),theory(equality)],[1,370]),
[iquote('0:Res:1.0,370.0')] ).
cnf(717,plain,
append_succeeds(skc4,u,skf286(u,skc4)),
inference(res,[status(thm),theory(equality)],[1,185]),
[iquote('0:Res:1.0,185.0')] ).
cnf(759,plain,
( ~ list_succeeds(skc4)
| ~ equal(rev(rev(skc295)),skc295) ),
inference(res,[status(thm),theory(equality)],[440,33]),
[iquote('0:Res:440.2,33.0')] ).
cnf(791,plain,
( ~ append_succeeds(u,skc4,v)
| ~ append_succeeds(u,rev(rev(skc4)),v) ),
inference(res,[status(thm),theory(equality)],[395,33]),
[iquote('0:Res:395.2,33.0')] ).
cnf(841,plain,
~ equal(rev(rev(skc295)),skc295),
inference(mrr,[status(thm)],[759,1]),
[iquote('0:MRR:759.0,1.0')] ).
cnf(897,plain,
equal(skc4,nil),
inference(spt,[spt(split,[position(s1)])],[684]),
[iquote('1:Spt:684.0')] ).
cnf(909,plain,
( ~ append_succeeds(u,skc4,v)
| ~ append_succeeds(u,rev(rev(nil)),v) ),
inference(rew,[status(thm),theory(equality)],[897,791]),
[iquote('1:Rew:897.0,791.1')] ).
cnf(1017,plain,
append_succeeds(nil,u,skf286(u,nil)),
inference(rew,[status(thm),theory(equality)],[897,717]),
[iquote('1:Rew:897.0,717.0')] ).
cnf(1161,plain,
( ~ append_succeeds(u,nil,v)
| ~ append_succeeds(u,nil,v) ),
inference(rew,[status(thm),theory(equality)],[18,909,897]),
[iquote('1:Rew:18.0,909.1,18.0,909.1,897.0,909.0')] ).
cnf(1162,plain,
~ append_succeeds(u,nil,v),
inference(obv,[status(thm),theory(equality)],[1161]),
[iquote('1:Obv:1161.0')] ).
cnf(1163,plain,
$false,
inference(unc,[status(thm)],[1162,1017]),
[iquote('1:UnC:1162.0,1017.0')] ).
cnf(1243,plain,
~ equal(skc4,nil),
inference(spt,[spt(split,[position(sa)])],[1163,897]),
[iquote('1:Spt:1163.0,684.0,897.0')] ).
cnf(1244,plain,
equal(cons(skf238(skc4),skf237(skc4)),skc4),
inference(spt,[spt(split,[position(s2)])],[684]),
[iquote('1:Spt:1163.0,684.1')] ).
cnf(1319,plain,
( ~ list_succeeds(u)
| list_succeeds(skf302(u)) ),
inference(res,[status(thm),theory(equality)],[117,68]),
[iquote('0:Res:117.1,68.0')] ).
cnf(1554,plain,
equal(skc295,nil),
inference(spt,[spt(split,[position(s2s1)])],[162]),
[iquote('2:Spt:162.0')] ).
cnf(1555,plain,
~ equal(rev(rev(nil)),nil),
inference(rew,[status(thm),theory(equality)],[1554,841]),
[iquote('2:Rew:1554.0,841.0')] ).
cnf(1556,plain,
~ equal(nil,nil),
inference(rew,[status(thm),theory(equality)],[18,1555]),
[iquote('2:Rew:18.0,1555.0,18.0,1555.0')] ).
cnf(1557,plain,
$false,
inference(obv,[status(thm),theory(equality)],[1556]),
[iquote('2:Obv:1556.0')] ).
cnf(1558,plain,
~ equal(skc295,nil),
inference(spt,[spt(split,[position(s2sa)])],[1557,1554]),
[iquote('2:Spt:1557.0,162.0,1554.0')] ).
cnf(1559,plain,
equal(rev(rev(skc296)),skc296),
inference(spt,[spt(split,[position(s2s2)])],[162]),
[iquote('2:Spt:1557.0,162.1')] ).
cnf(1560,plain,
equal(cons(skc297,skc296),skc295),
inference(mrr,[status(thm)],[161,1558]),
[iquote('2:MRR:161.0,1558.0')] ).
cnf(1792,plain,
( ~ list_succeeds(u)
| equal(rev(u),skf302(u)) ),
inference(res,[status(thm),theory(equality)],[117,636]),
[iquote('0:Res:117.1,636.0')] ).
cnf(1795,plain,
( ~ list_succeeds(u)
| equal(a42__a42_(skf302(u),cons(v,nil)),rev(cons(v,u))) ),
inference(rew,[status(thm),theory(equality)],[1792,438]),
[iquote('0:Rew:1792.1,438.1')] ).
cnf(1796,plain,
( ~ list_succeeds(u)
| equal(cons(v,skf302(u)),rev(a42__a42_(u,cons(v,nil)))) ),
inference(rew,[status(thm),theory(equality)],[1792,439]),
[iquote('0:Rew:1792.1,439.1')] ).
cnf(1825,plain,
( ~ list_succeeds(skc296)
| equal(rev(skf302(skc296)),skc296) ),
inference(spr,[status(thm),theory(equality)],[1792,1559]),
[iquote('2:SpR:1792.1,1559.0')] ).
cnf(1834,plain,
equal(rev(skf302(skc296)),skc296),
inference(ssi,[status(thm)],[1825,4]),
[iquote('2:SSi:1825.0,4.0')] ).
cnf(1861,plain,
( ~ list_succeeds(skf302(skc296))
| equal(skf302(skf302(skc296)),skc296) ),
inference(spr,[status(thm),theory(equality)],[1834,1792]),
[iquote('2:SpR:1834.0,1792.1')] ).
cnf(1863,plain,
equal(skf302(skf302(skc296)),skc296),
inference(ssi,[status(thm)],[1861,1319,4]),
[iquote('2:SSi:1861.0,1319.0,4.1')] ).
cnf(11374,plain,
( ~ list_succeeds(skc296)
| equal(a42__a42_(skf302(skc296),cons(skc297,nil)),rev(skc295)) ),
inference(spr,[status(thm),theory(equality)],[1560,1795]),
[iquote('2:SpR:1560.0,1795.1')] ).
cnf(11676,plain,
( ~ list_succeeds(skf302(skc296))
| equal(cons(u,skc296),rev(a42__a42_(skf302(skc296),cons(u,nil)))) ),
inference(spr,[status(thm),theory(equality)],[1863,1796]),
[iquote('2:SpR:1863.0,1796.1')] ).
cnf(11862,plain,
equal(a42__a42_(skf302(skc296),cons(skc297,nil)),rev(skc295)),
inference(ssi,[status(thm)],[11374,4]),
[iquote('2:SSi:11374.0,4.0')] ).
cnf(11865,plain,
equal(cons(u,skc296),rev(a42__a42_(skf302(skc296),cons(u,nil)))),
inference(ssi,[status(thm)],[11676,1319,4]),
[iquote('2:SSi:11676.0,1319.0,4.1')] ).
cnf(11866,plain,
equal(rev(a42__a42_(skf302(skc296),cons(skc297,nil))),skc295),
inference(rew,[status(thm),theory(equality)],[11865,1560]),
[iquote('2:Rew:11865.0,1560.0')] ).
cnf(11867,plain,
equal(rev(rev(skc295)),skc295),
inference(rew,[status(thm),theory(equality)],[11862,11866]),
[iquote('2:Rew:11862.0,11866.0')] ).
cnf(11868,plain,
$false,
inference(mrr,[status(thm)],[11867,841]),
[iquote('2:MRR:11867.0,841.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SWX063+1 : TPTP v9.1.0. Released v9.1.0.
% 0.08/0.15 % Command : run_spass %d %s
% 0.14/0.36 % Computer : n028.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Mon Mar 31 15:33:04 EDT 2025
% 0.14/0.36 % CPUTime :
% 6.79/6.97
% 6.79/6.97 SPASS V 3.9
% 6.79/6.97 SPASS beiseite: Proof found.
% 6.79/6.97 % SZS status Theorem
% 6.79/6.97 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.79/6.97 SPASS derived 9588 clauses, backtracked 1344 clauses, performed 28 splits and kept 6533 clauses.
% 6.79/6.97 SPASS allocated 109284 KBytes.
% 6.79/6.97 SPASS spent 0:00:06.48 on the problem.
% 6.79/6.97 0:00:00.04 for the input.
% 6.79/6.97 0:00:01.92 for the FLOTTER CNF translation.
% 6.79/6.97 0:00:00.15 for inferences.
% 6.79/6.97 0:00:00.22 for the backtracking.
% 6.79/6.97 0:00:03.89 for the reduction.
% 6.79/6.97
% 6.79/6.97
% 6.79/6.97 Here is a proof with depth 4, length 52 :
% 6.79/6.97 % SZS output start Refutation
% See solution above
% 6.79/6.97 Formulae used in the proof : theorem_a45__a40_rev_a58_involution_a41_ induction corollary_a45__a40_rev_a58_nil_a41_ lemma_a45__a40_n_reverse_a58_types_a41_ lemma_a45__a40_n_reverse_a58_existence_a41_ axiom_a45__a40_append_a58_existence_a41_ rev_a47_1 id88 axiom_a45__a40_append_a58_uniqueness_a58_2_a41_ corollary_a45__a40_rev_a58_cons_a41_ lemma_a45__a40_rev_a58_app_a41_
% 6.79/6.97
%------------------------------------------------------------------------------