%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LCL162-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 01:06:54 PM UTC 2026
% Result : Unsatisfiable 12.66s 13.01s
% Output : Refutation 13.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 13
% Syntax : Number of clauses : 82 ( 82 unt; 0 nHn; 82 RR)
% Number of literals : 82 ( 0 equ; 3 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 : 12 ( 12 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(xor__dfg(u,v),xor__dfg(v,u)),
file('LCL162-1.p',unknown),
[] ).
cnf(2,axiom,
equal(and_star(and_star(u,v),w),and_star(u,and_star(v,w))),
file('LCL162-1.p',unknown),
[] ).
cnf(3,axiom,
equal(and_star(u,v),and_star(v,u)),
file('LCL162-1.p',unknown),
[] ).
cnf(4,axiom,
equal(not__dfg(truth),falsehood),
file('LCL162-1.p',unknown),
[] ).
cnf(5,axiom,
equal(xor__dfg(truth,and_star(u,xor__dfg(truth,v))),implies__dfg(u,v)),
file('LCL162-1.p',unknown),
[] ).
cnf(6,axiom,
~ equal(implies__dfg(implies__dfg(x__dfg,y__dfg),implies__dfg(implies__dfg(y__dfg,z__dfg),implies__dfg(x__dfg,z__dfg))),truth),
file('LCL162-1.p',unknown),
[] ).
cnf(7,axiom,
equal(xor__dfg(u,truth),not__dfg(u)),
file('LCL162-1.p',unknown),
[] ).
cnf(8,axiom,
equal(xor__dfg(u,falsehood),u),
file('LCL162-1.p',unknown),
[] ).
cnf(10,axiom,
equal(and_star(u,truth),u),
file('LCL162-1.p',unknown),
[] ).
cnf(11,axiom,
equal(and_star(u,falsehood),falsehood),
file('LCL162-1.p',unknown),
[] ).
cnf(12,axiom,
equal(and_star(xor__dfg(truth,u),u),falsehood),
file('LCL162-1.p',unknown),
[] ).
cnf(13,axiom,
equal(xor__dfg(xor__dfg(u,truth),v),xor__dfg(u,xor__dfg(truth,v))),
file('LCL162-1.p',unknown),
[] ).
cnf(14,axiom,
equal(and_star(xor__dfg(and_star(xor__dfg(truth,u),v),truth),v),and_star(xor__dfg(and_star(xor__dfg(truth,v),u),truth),u)),
file('LCL162-1.p',unknown),
[] ).
cnf(15,plain,
equal(and_star(u,xor__dfg(truth,u)),falsehood),
inference(rew,[status(thm),theory(equality)],[3,12]),
[iquote('0:Rew:3.0,12.0')] ).
cnf(16,plain,
equal(xor__dfg(u,xor__dfg(truth,v)),xor__dfg(not__dfg(u),v)),
inference(rew,[status(thm),theory(equality)],[7,13]),
[iquote('0:Rew:7.0,13.0')] ).
cnf(17,plain,
equal(and_star(u,xor__dfg(truth,and_star(xor__dfg(truth,v),u))),and_star(v,xor__dfg(truth,and_star(xor__dfg(truth,u),v)))),
inference(rew,[status(thm),theory(equality)],[3,14,1]),
[iquote('0:Rew:3.0,14.0,1.0,14.0,3.0,14.0,1.0,14.0')] ).
cnf(32,plain,
equal(and_star(truth,u),u),
inference(spr,[status(thm),theory(equality)],[3,10]),
[iquote('0:SpR:3.0,10.0')] ).
cnf(45,plain,
equal(xor__dfg(falsehood,u),u),
inference(spr,[status(thm),theory(equality)],[1,8]),
[iquote('0:SpR:1.0,8.0')] ).
cnf(47,plain,
equal(xor__dfg(truth,u),not__dfg(u)),
inference(spr,[status(thm),theory(equality)],[1,7]),
[iquote('0:SpR:1.0,7.0')] ).
cnf(57,plain,
equal(and_star(u,not__dfg(u)),falsehood),
inference(rew,[status(thm),theory(equality)],[47,15]),
[iquote('0:Rew:47.0,15.0')] ).
cnf(58,plain,
equal(and_star(u,not__dfg(and_star(xor__dfg(truth,v),u))),and_star(v,xor__dfg(truth,and_star(xor__dfg(truth,u),v)))),
inference(rew,[status(thm),theory(equality)],[47,17]),
[iquote('0:Rew:47.0,17.0')] ).
cnf(59,plain,
equal(not__dfg(and_star(u,xor__dfg(truth,v))),implies__dfg(u,v)),
inference(rew,[status(thm),theory(equality)],[47,5]),
[iquote('0:Rew:47.0,5.0')] ).
cnf(60,plain,
equal(xor__dfg(not__dfg(u),v),xor__dfg(u,not__dfg(v))),
inference(rew,[status(thm),theory(equality)],[47,16]),
[iquote('0:Rew:47.0,16.0')] ).
cnf(63,plain,
equal(not__dfg(and_star(u,not__dfg(v))),implies__dfg(u,v)),
inference(rew,[status(thm),theory(equality)],[47,59]),
[iquote('0:Rew:47.0,59.0')] ).
cnf(64,plain,
equal(and_star(u,not__dfg(and_star(not__dfg(v),u))),and_star(v,not__dfg(and_star(not__dfg(u),v)))),
inference(rew,[status(thm),theory(equality)],[47,58]),
[iquote('0:Rew:47.0,58.0,47.0,58.0,47.0,58.0')] ).
cnf(72,plain,
equal(not__dfg(falsehood),truth),
inference(spr,[status(thm),theory(equality)],[45,7]),
[iquote('0:SpR:45.0,7.0')] ).
cnf(90,plain,
equal(xor__dfg(u,not__dfg(truth)),not__dfg(not__dfg(u))),
inference(spr,[status(thm),theory(equality)],[60,7]),
[iquote('0:SpR:60.0,7.0')] ).
cnf(97,plain,
equal(not__dfg(not__dfg(u)),u),
inference(rew,[status(thm),theory(equality)],[8,90,4]),
[iquote('0:Rew:8.0,90.0,4.0,90.0')] ).
cnf(111,plain,
equal(and_star(u,not__dfg(v)),not__dfg(implies__dfg(u,v))),
inference(spr,[status(thm),theory(equality)],[63,97]),
[iquote('0:SpR:63.0,97.0')] ).
cnf(114,plain,
equal(not__dfg(and_star(u,falsehood)),implies__dfg(u,truth)),
inference(spr,[status(thm),theory(equality)],[4,63]),
[iquote('0:SpR:4.0,63.0')] ).
cnf(116,plain,
equal(implies__dfg(u,not__dfg(v)),not__dfg(and_star(u,v))),
inference(spr,[status(thm),theory(equality)],[97,63]),
[iquote('0:SpR:97.0,63.0')] ).
cnf(117,plain,
equal(not__dfg(and_star(not__dfg(u),v)),implies__dfg(v,u)),
inference(spr,[status(thm),theory(equality)],[3,63]),
[iquote('0:SpR:3.0,63.0')] ).
cnf(118,plain,
equal(implies__dfg(u,u),not__dfg(falsehood)),
inference(spr,[status(thm),theory(equality)],[57,63]),
[iquote('0:SpR:57.0,63.0')] ).
cnf(122,plain,
equal(implies__dfg(u,u),truth),
inference(rew,[status(thm),theory(equality)],[72,118]),
[iquote('0:Rew:72.0,118.0')] ).
cnf(125,plain,
equal(implies__dfg(u,truth),truth),
inference(rew,[status(thm),theory(equality)],[72,114,11]),
[iquote('0:Rew:72.0,114.0,11.0,114.0')] ).
cnf(129,plain,
equal(and_star(u,not__dfg(and_star(not__dfg(v),u))),not__dfg(implies__dfg(v,and_star(not__dfg(u),v)))),
inference(rew,[status(thm),theory(equality)],[111,64]),
[iquote('0:Rew:111.0,64.0')] ).
cnf(136,plain,
equal(and_star(u,implies__dfg(u,v)),not__dfg(implies__dfg(v,and_star(not__dfg(u),v)))),
inference(rew,[status(thm),theory(equality)],[117,129]),
[iquote('0:Rew:117.0,129.0')] ).
cnf(172,plain,
equal(not__dfg(implies__dfg(u,and_star(not__dfg(and_star(v,w)),u))),and_star(v,and_star(w,implies__dfg(and_star(v,w),u)))),
inference(spr,[status(thm),theory(equality)],[136,2]),
[iquote('0:SpR:136.0,2.0')] ).
cnf(173,plain,
equal(and_star(u,implies__dfg(u,implies__dfg(not__dfg(u),v))),not__dfg(implies__dfg(implies__dfg(not__dfg(u),v),not__dfg(implies__dfg(v,and_star(not__dfg(not__dfg(u)),v)))))),
inference(spr,[status(thm),theory(equality)],[136]),
[iquote('0:SpR:136.0,136.0')] ).
cnf(207,plain,
equal(and_star(u,implies__dfg(u,implies__dfg(not__dfg(u),v))),not__dfg(implies__dfg(implies__dfg(not__dfg(u),v),not__dfg(implies__dfg(v,and_star(u,v)))))),
inference(rew,[status(thm),theory(equality)],[97,173]),
[iquote('0:Rew:97.0,173.0')] ).
cnf(208,plain,
equal(and_star(u,implies__dfg(u,implies__dfg(not__dfg(u),v))),not__dfg(not__dfg(and_star(implies__dfg(not__dfg(u),v),implies__dfg(v,and_star(u,v)))))),
inference(rew,[status(thm),theory(equality)],[116,207]),
[iquote('0:Rew:116.0,207.0')] ).
cnf(209,plain,
equal(and_star(u,implies__dfg(u,implies__dfg(not__dfg(u),v))),and_star(implies__dfg(not__dfg(u),v),implies__dfg(v,and_star(u,v)))),
inference(rew,[status(thm),theory(equality)],[97,208]),
[iquote('0:Rew:97.0,208.0')] ).
cnf(249,plain,
equal(and_star(not__dfg(u),v),not__dfg(implies__dfg(v,u))),
inference(spr,[status(thm),theory(equality)],[111,3]),
[iquote('0:SpR:111.0,3.0')] ).
cnf(250,plain,
equal(and_star(not__dfg(implies__dfg(u,v)),w),and_star(u,and_star(not__dfg(v),w))),
inference(spr,[status(thm),theory(equality)],[111,2]),
[iquote('0:SpR:111.0,2.0')] ).
cnf(268,plain,
equal(not__dfg(implies__dfg(u,not__dfg(implies__dfg(u,and_star(v,w))))),and_star(v,and_star(w,implies__dfg(and_star(v,w),u)))),
inference(rew,[status(thm),theory(equality)],[249,172]),
[iquote('0:Rew:249.0,172.0')] ).
cnf(275,plain,
equal(and_star(u,not__dfg(implies__dfg(v,w))),not__dfg(implies__dfg(v,implies__dfg(u,w)))),
inference(rew,[status(thm),theory(equality)],[249,250]),
[iquote('0:Rew:249.0,250.0,249.0,250.0')] ).
cnf(276,plain,
equal(not__dfg(implies__dfg(u,implies__dfg(v,w))),not__dfg(implies__dfg(v,implies__dfg(u,w)))),
inference(rew,[status(thm),theory(equality)],[111,275]),
[iquote('0:Rew:111.0,275.0')] ).
cnf(291,plain,
equal(not__dfg(not__dfg(and_star(u,implies__dfg(u,and_star(v,w))))),and_star(v,and_star(w,implies__dfg(and_star(v,w),u)))),
inference(rew,[status(thm),theory(equality)],[116,268]),
[iquote('0:Rew:116.0,268.0')] ).
cnf(292,plain,
equal(and_star(u,implies__dfg(u,and_star(v,w))),and_star(v,and_star(w,implies__dfg(and_star(v,w),u)))),
inference(rew,[status(thm),theory(equality)],[97,291]),
[iquote('0:Rew:97.0,291.0')] ).
cnf(311,plain,
equal(not__dfg(implies__dfg(not__dfg(u),v)),not__dfg(implies__dfg(not__dfg(v),u))),
inference(spr,[status(thm),theory(equality)],[249,111]),
[iquote('0:SpR:249.0,111.0')] ).
cnf(325,plain,
equal(not__dfg(not__dfg(implies__dfg(not__dfg(u),v))),implies__dfg(not__dfg(v),u)),
inference(spr,[status(thm),theory(equality)],[311,97]),
[iquote('0:SpR:311.0,97.0')] ).
cnf(366,plain,
equal(implies__dfg(not__dfg(u),v),implies__dfg(not__dfg(v),u)),
inference(rew,[status(thm),theory(equality)],[97,325]),
[iquote('0:Rew:97.0,325.0')] ).
cnf(876,plain,
equal(not__dfg(not__dfg(implies__dfg(u,implies__dfg(v,w)))),implies__dfg(v,implies__dfg(u,w))),
inference(spr,[status(thm),theory(equality)],[276,97]),
[iquote('0:SpR:276.0,97.0')] ).
cnf(909,plain,
equal(not__dfg(implies__dfg(u,implies__dfg(v,u))),not__dfg(implies__dfg(v,truth))),
inference(spr,[status(thm),theory(equality)],[122,276]),
[iquote('0:SpR:122.0,276.0')] ).
cnf(936,plain,
equal(not__dfg(implies__dfg(u,implies__dfg(v,u))),falsehood),
inference(rew,[status(thm),theory(equality)],[4,909,125]),
[iquote('0:Rew:4.0,909.0,125.0,909.0')] ).
cnf(947,plain,
equal(implies__dfg(u,implies__dfg(v,w)),implies__dfg(v,implies__dfg(u,w))),
inference(rew,[status(thm),theory(equality)],[97,876]),
[iquote('0:Rew:97.0,876.0')] ).
cnf(948,plain,
~ equal(implies__dfg(implies__dfg(x__dfg,y__dfg),implies__dfg(x__dfg,implies__dfg(implies__dfg(y__dfg,z__dfg),z__dfg))),truth),
inference(rew,[status(thm),theory(equality)],[947,6]),
[iquote('0:Rew:947.0,6.0')] ).
cnf(950,plain,
~ equal(implies__dfg(x__dfg,implies__dfg(implies__dfg(x__dfg,y__dfg),implies__dfg(implies__dfg(y__dfg,z__dfg),z__dfg))),truth),
inference(rew,[status(thm),theory(equality)],[947,948]),
[iquote('0:Rew:947.0,948.0')] ).
cnf(967,plain,
equal(implies__dfg(u,implies__dfg(v,u)),not__dfg(falsehood)),
inference(spr,[status(thm),theory(equality)],[936,97]),
[iquote('0:SpR:936.0,97.0')] ).
cnf(996,plain,
equal(implies__dfg(u,implies__dfg(v,u)),truth),
inference(rew,[status(thm),theory(equality)],[72,967]),
[iquote('0:Rew:72.0,967.0')] ).
cnf(1033,plain,
equal(not__dfg(implies__dfg(u,implies__dfg(v,implies__dfg(w,u)))),not__dfg(implies__dfg(v,truth))),
inference(spr,[status(thm),theory(equality)],[996,276]),
[iquote('0:SpR:996.0,276.0')] ).
cnf(1040,plain,
equal(implies__dfg(u,implies__dfg(not__dfg(u),v)),truth),
inference(spr,[status(thm),theory(equality)],[366,996]),
[iquote('0:SpR:366.0,996.0')] ).
cnf(1046,plain,
equal(and_star(implies__dfg(not__dfg(u),v),implies__dfg(v,and_star(u,v))),and_star(u,truth)),
inference(rew,[status(thm),theory(equality)],[1040,209]),
[iquote('0:Rew:1040.0,209.0')] ).
cnf(1051,plain,
equal(not__dfg(implies__dfg(u,implies__dfg(v,implies__dfg(w,u)))),falsehood),
inference(rew,[status(thm),theory(equality)],[4,1033,125]),
[iquote('0:Rew:4.0,1033.0,125.0,1033.0')] ).
cnf(1053,plain,
equal(and_star(implies__dfg(not__dfg(u),v),implies__dfg(v,and_star(u,v))),u),
inference(rew,[status(thm),theory(equality)],[10,1046]),
[iquote('0:Rew:10.0,1046.0')] ).
cnf(1204,plain,
equal(and_star(implies__dfg(not__dfg(u),not__dfg(v)),implies__dfg(not__dfg(v),not__dfg(implies__dfg(u,v)))),u),
inference(spr,[status(thm),theory(equality)],[111,1053]),
[iquote('0:SpR:111.0,1053.0')] ).
cnf(1246,plain,
equal(and_star(implies__dfg(u,v),implies__dfg(implies__dfg(v,u),u)),v),
inference(rew,[status(thm),theory(equality)],[97,1204,249,116]),
[iquote('0:Rew:97.0,1204.0,249.0,1204.0,116.0,1204.0,97.0,1204.0,249.0,1204.0,116.0,1204.0')] ).
cnf(1655,plain,
equal(implies__dfg(u,implies__dfg(v,implies__dfg(w,u))),not__dfg(falsehood)),
inference(spr,[status(thm),theory(equality)],[1051,97]),
[iquote('0:SpR:1051.0,97.0')] ).
cnf(1719,plain,
equal(implies__dfg(u,implies__dfg(v,implies__dfg(w,u))),truth),
inference(rew,[status(thm),theory(equality)],[72,1655]),
[iquote('0:Rew:72.0,1655.0')] ).
cnf(1786,plain,
equal(implies__dfg(not__dfg(u),implies__dfg(v,not__dfg(and_star(w,u)))),truth),
inference(spr,[status(thm),theory(equality)],[116,1719]),
[iquote('0:SpR:116.0,1719.0')] ).
cnf(1821,plain,
equal(implies__dfg(and_star(u,and_star(v,w)),w),truth),
inference(rew,[status(thm),theory(equality)],[97,1786,249,116]),
[iquote('0:Rew:97.0,1786.0,249.0,1786.0,116.0,1786.0,116.0,1786.0')] ).
cnf(1857,plain,
equal(implies__dfg(and_star(u,v),v),truth),
inference(spr,[status(thm),theory(equality)],[32,1821]),
[iquote('0:SpR:32.0,1821.0')] ).
cnf(1933,plain,
equal(implies__dfg(and_star(u,v),u),truth),
inference(spr,[status(thm),theory(equality)],[3,1857]),
[iquote('0:SpR:3.0,1857.0')] ).
cnf(2411,plain,
equal(implies__dfg(and_star(u,implies__dfg(u,and_star(v,w))),v),truth),
inference(spr,[status(thm),theory(equality)],[292,1933]),
[iquote('0:SpR:292.0,1933.0')] ).
cnf(6690,plain,
equal(not__dfg(and_star(and_star(u,implies__dfg(u,and_star(not__dfg(v),w))),v)),truth),
inference(spr,[status(thm),theory(equality)],[2411,116]),
[iquote('0:SpR:2411.0,116.0')] ).
cnf(6783,plain,
equal(implies__dfg(u,implies__dfg(v,and_star(v,implies__dfg(w,u)))),truth),
inference(rew,[status(thm),theory(equality)],[97,6690,249,111,116]),
[iquote('0:Rew:97.0,6690.0,249.0,6690.0,111.0,6690.0,116.0,6690.0,249.0,6690.0')] ).
cnf(12768,plain,
equal(implies__dfg(u,implies__dfg(v,and_star(implies__dfg(w,u),v))),truth),
inference(spr,[status(thm),theory(equality)],[3,6783]),
[iquote('0:SpR:3.0,6783.0')] ).
cnf(15738,plain,
equal(implies__dfg(u,implies__dfg(v,and_star(implies__dfg(w,v),u))),truth),
inference(spr,[status(thm),theory(equality)],[947,12768]),
[iquote('0:SpR:947.0,12768.0')] ).
cnf(16709,plain,
equal(implies__dfg(u,implies__dfg(not__dfg(v),and_star(not__dfg(and_star(w,v)),u))),truth),
inference(spr,[status(thm),theory(equality)],[116,15738]),
[iquote('0:SpR:116.0,15738.0')] ).
cnf(16840,plain,
equal(implies__dfg(u,implies__dfg(implies__dfg(u,and_star(v,w)),w)),truth),
inference(rew,[status(thm),theory(equality)],[97,16709,249,116]),
[iquote('0:Rew:97.0,16709.0,249.0,16709.0,116.0,16709.0,249.0,16709.0')] ).
cnf(21363,plain,
equal(implies__dfg(u,implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(v,w),w))),truth),
inference(spr,[status(thm),theory(equality)],[1246,16840]),
[iquote('0:SpR:1246.0,16840.0')] ).
cnf(21608,plain,
$false,
inference(unc,[status(thm)],[21363,950]),
[iquote('0:UnC:21363.0,950.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL162-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_spass %d %s
% 0.11/0.37 % Computer : n029.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 4 19:22:24 UTC 2026
% 0.11/0.37 % CPUTime :
% 12.66/13.01
% 12.66/13.01 SPASS V 3.9
% 12.66/13.01 SPASS beiseite: Proof found.
% 12.66/13.01 % SZS status Theorem
% 12.66/13.01 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.66/13.01 SPASS derived 13531 clauses, backtracked 0 clauses, performed 0 splits and kept 2309 clauses.
% 12.66/13.01 SPASS allocated 83461 KBytes.
% 12.66/13.01 SPASS spent 0:0:12.59 on the problem.
% 12.66/13.01 0:00:00.06 for the input.
% 12.66/13.01 0:00:00.00 for the FLOTTER CNF translation.
% 12.66/13.01 0:00:00.21 for inferences.
% 12.66/13.01 0:00:00.00 for the backtracking.
% 12.66/13.01 0:0:12.27 for the reduction.
% 12.66/13.01
% 12.66/13.01
% 12.66/13.01 Here is a proof with depth 16, length 82 :
% 12.66/13.01 % SZS output start Refutation
% See solution above
% 13.06/13.36 Formulae used in the proof : xor_commutativity and_star_associativity and_star_commutativity false_definition implies_definition prove_wajsberg_axiom axiom_1 axiom_2 axiom_4 axiom_5 axiom_6 axiom_7 axiom_8
% 13.06/13.36
%------------------------------------------------------------------------------