%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SEU305+2 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n027.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 : Tue Jul 19 14:36:05 EDT 2022
% Result : Theorem 75.81s 75.99s
% Output : Refutation 75.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 11
% Syntax : Number of clauses : 28 ( 17 unt; 8 nHn; 28 RR)
% Number of literals : 66 ( 0 equ; 32 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
join_commutative(skc30),
file('SEU305+2.p',unknown),
[] ).
cnf(2,axiom,
join_semilatt_str(skc30),
file('SEU305+2.p',unknown),
[] ).
cnf(73,axiom,
~ empty_carrier(skc30),
file('SEU305+2.p',unknown),
[] ).
cnf(120,axiom,
element(skc32,the_carrier(skc30)),
file('SEU305+2.p',unknown),
[] ).
cnf(121,axiom,
element(skc31,the_carrier(skc30)),
file('SEU305+2.p',unknown),
[] ).
cnf(122,axiom,
below(skc30,skc31,skc32),
file('SEU305+2.p',unknown),
[] ).
cnf(123,axiom,
below(skc30,skc32,skc31),
file('SEU305+2.p',unknown),
[] ).
cnf(124,axiom,
~ equal(skc32,skc31),
file('SEU305+2.p',unknown),
[] ).
cnf(998,axiom,
( ~ join_semilatt_str(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ below(u,w,v)
| empty_carrier(u)
| equal(join(u,w,v),v) ),
file('SEU305+2.p',unknown),
[] ).
cnf(1013,axiom,
( ~ join_semilatt_str(u)
| ~ join_commutative(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty_carrier(u)
| equal(join(u,w,v),join_commut(u,w,v)) ),
file('SEU305+2.p',unknown),
[] ).
cnf(1019,axiom,
( ~ join_semilatt_str(u)
| ~ join_commutative(u)
| ~ element(v,the_carrier(u))
| ~ element(w,the_carrier(u))
| empty_carrier(u)
| equal(join_commut(u,w,v),join_commut(u,v,w)) ),
file('SEU305+2.p',unknown),
[] ).
cnf(1313,plain,
( ~ join_semilatt_str(skc30)
| ~ element(skc32,the_carrier(skc30))
| ~ element(skc31,the_carrier(skc30))
| equal(join(skc30,skc32,skc31),skc31)
| empty_carrier(skc30) ),
inference(res,[status(thm),theory(equality)],[123,998]),
[iquote('0:Res:123.0,998.1')] ).
cnf(1314,plain,
( ~ join_semilatt_str(skc30)
| ~ element(skc31,the_carrier(skc30))
| ~ element(skc32,the_carrier(skc30))
| equal(join(skc30,skc31,skc32),skc32)
| empty_carrier(skc30) ),
inference(res,[status(thm),theory(equality)],[122,998]),
[iquote('0:Res:122.0,998.1')] ).
cnf(1325,plain,
( ~ join_commutative(skc30)
| ~ join_semilatt_str(skc30)
| ~ element(u,the_carrier(skc30))
| equal(join(skc30,skc31,u),join_commut(skc30,skc31,u))
| empty_carrier(skc30) ),
inference(res,[status(thm),theory(equality)],[121,1013]),
[iquote('0:Res:121.0,1013.2')] ).
cnf(1336,plain,
( ~ join_commutative(skc30)
| ~ join_semilatt_str(skc30)
| ~ element(u,the_carrier(skc30))
| equal(join_commut(skc30,u,skc31),join_commut(skc30,skc31,u))
| empty_carrier(skc30) ),
inference(res,[status(thm),theory(equality)],[121,1019]),
[iquote('0:Res:121.0,1019.3')] ).
cnf(1339,plain,
( ~ join_commutative(skc30)
| ~ join_semilatt_str(skc30)
| ~ element(u,the_carrier(skc30))
| equal(join(skc30,u,skc31),join_commut(skc30,u,skc31))
| empty_carrier(skc30) ),
inference(res,[status(thm),theory(equality)],[121,1013]),
[iquote('0:Res:121.0,1013.3')] ).
cnf(1421,plain,
equal(join(skc30,skc31,skc32),skc32),
inference(mrr,[status(thm)],[1314,2,121,120,73]),
[iquote('0:MRR:1314.0,1314.1,1314.2,1314.4,2.0,121.0,120.0,73.0')] ).
cnf(1422,plain,
equal(join(skc30,skc32,skc31),skc31),
inference(mrr,[status(thm)],[1313,2,120,121,73]),
[iquote('0:MRR:1313.0,1313.1,1313.2,1313.4,2.0,120.0,121.0,73.0')] ).
cnf(1438,plain,
( ~ element(u,the_carrier(skc30))
| equal(join(skc30,u,skc31),join_commut(skc30,u,skc31)) ),
inference(mrr,[status(thm)],[1339,1,2,73]),
[iquote('0:MRR:1339.0,1339.1,1339.4,1.0,2.0,73.0')] ).
cnf(1444,plain,
( ~ element(u,the_carrier(skc30))
| equal(join_commut(skc30,u,skc31),join_commut(skc30,skc31,u)) ),
inference(mrr,[status(thm)],[1336,1,2,73]),
[iquote('0:MRR:1336.0,1336.1,1336.4,1.0,2.0,73.0')] ).
cnf(1446,plain,
( ~ element(u,the_carrier(skc30))
| equal(join(skc30,skc31,u),join_commut(skc30,skc31,u)) ),
inference(mrr,[status(thm)],[1325,1,2,73]),
[iquote('0:MRR:1325.0,1325.1,1325.4,1.0,2.0,73.0')] ).
cnf(1518,plain,
equal(join(skc30,skc31,skc32),join_commut(skc30,skc31,skc32)),
inference(res,[status(thm),theory(equality)],[120,1446]),
[iquote('0:Res:120.0,1446.0')] ).
cnf(1520,plain,
equal(join_commut(skc30,skc32,skc31),join_commut(skc30,skc31,skc32)),
inference(res,[status(thm),theory(equality)],[120,1444]),
[iquote('0:Res:120.0,1444.0')] ).
cnf(1525,plain,
equal(join(skc30,skc32,skc31),join_commut(skc30,skc32,skc31)),
inference(res,[status(thm),theory(equality)],[120,1438]),
[iquote('0:Res:120.0,1438.0')] ).
cnf(1656,plain,
equal(join_commut(skc30,skc31,skc32),skc32),
inference(rew,[status(thm),theory(equality)],[1421,1518]),
[iquote('0:Rew:1421.0,1518.0')] ).
cnf(1658,plain,
equal(join_commut(skc30,skc32,skc31),skc32),
inference(rew,[status(thm),theory(equality)],[1656,1520]),
[iquote('0:Rew:1656.0,1520.0')] ).
cnf(1660,plain,
equal(skc32,skc31),
inference(rew,[status(thm),theory(equality)],[1422,1525,1658]),
[iquote('0:Rew:1422.0,1525.0,1658.0,1525.0')] ).
cnf(1661,plain,
$false,
inference(mrr,[status(thm)],[1660,124]),
[iquote('0:MRR:1660.0,124.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU305+2 : TPTP v8.1.0. Released v3.3.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n027.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 : Mon Jun 20 12:32:40 EDT 2022
% 0.12/0.33 % CPUTime :
% 75.81/75.99
% 75.81/75.99 SPASS V 3.9
% 75.81/75.99 SPASS beiseite: Proof found.
% 75.81/75.99 % SZS status Theorem
% 75.81/75.99 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 75.81/75.99 SPASS derived 361 clauses, backtracked 0 clauses, performed 0 splits and kept 1187 clauses.
% 75.81/75.99 SPASS allocated 159707 KBytes.
% 75.81/75.99 SPASS spent 0:1:15.61 on the problem.
% 75.81/75.99 0:00:00.04 for the input.
% 75.81/75.99 0:1:14.99 for the FLOTTER CNF translation.
% 75.81/75.99 0:00:00.00 for inferences.
% 75.81/75.99 0:00:00.00 for the backtracking.
% 75.81/75.99 0:00:00.30 for the reduction.
% 75.81/75.99
% 75.81/75.99
% 75.81/75.99 Here is a proof with depth 2, length 28 :
% 75.81/75.99 % SZS output start Refutation
% See solution above
% 75.81/75.99 Formulae used in the proof : t26_lattices d3_lattices redefinition_k3_lattices commutativity_k3_lattices
% 75.81/75.99
%------------------------------------------------------------------------------