%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SEU374+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n011.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:44 EDT 2022
% Result : Theorem 0.35s 0.53s
% Output : Refutation 0.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 14
% Syntax : Number of clauses : 26 ( 15 unt; 0 nHn; 26 RR)
% Number of literals : 65 ( 0 equ; 44 neg)
% Maximal clause size : 9 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 11 con; 0-1 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
one_sorted_str(skc16),
file('SEU374+1.p',unknown),
[] ).
cnf(28,axiom,
net_str(skc17,skc16),
file('SEU374+1.p',unknown),
[] ).
cnf(29,axiom,
equal(skc21,skc19),
file('SEU374+1.p',unknown),
[] ).
cnf(33,axiom,
element(skc21,the_carrier(skc18)),
file('SEU374+1.p',unknown),
[] ).
cnf(34,axiom,
element(skc20,the_carrier(skc17)),
file('SEU374+1.p',unknown),
[] ).
cnf(35,axiom,
element(skc19,the_carrier(skc17)),
file('SEU374+1.p',unknown),
[] ).
cnf(36,axiom,
subnetstr(skc18,skc16,skc17),
file('SEU374+1.p',unknown),
[] ).
cnf(37,axiom,
related(skc18,skc21,skc20),
file('SEU374+1.p',unknown),
[] ).
cnf(38,axiom,
element(skc20,the_carrier(skc18)),
file('SEU374+1.p',unknown),
[] ).
cnf(41,axiom,
~ related(skc17,skc19,skc20),
file('SEU374+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ one_sorted_str(u)
| ~ net_str(v,u)
| rel_str(v) ),
file('SEU374+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ one_sorted_str(u)
| ~ net_str(v,u)
| ~ subnetstr(w,u,v)
| net_str(w,u) ),
file('SEU374+1.p',unknown),
[] ).
cnf(82,axiom,
( ~ one_sorted_str(u)
| ~ subnetstr(v,u,w)
| ~ net_str(w,u)
| ~ net_str(v,u)
| subrelstr(v,w) ),
file('SEU374+1.p',unknown),
[] ).
cnf(85,axiom,
( ~ rel_str(u)
| ~ equal(v,w)
| ~ subrelstr(x,u)
| ~ element(y,the_carrier(x))
| ~ element(v,the_carrier(x))
| ~ element(y,the_carrier(u))
| ~ element(w,the_carrier(u))
| ~ related(x,v,y)
| related(u,w,y) ),
file('SEU374+1.p',unknown),
[] ).
cnf(86,plain,
related(skc18,skc19,skc20),
inference(rew,[status(thm),theory(equality)],[29,37]),
[iquote('0:Rew:29.0,37.0')] ).
cnf(87,plain,
element(skc19,the_carrier(skc18)),
inference(rew,[status(thm),theory(equality)],[29,33]),
[iquote('0:Rew:29.0,33.0')] ).
cnf(90,plain,
( ~ one_sorted_str(u)
| ~ net_str(v,u)
| ~ subnetstr(w,u,v)
| subrelstr(w,v) ),
inference(mrr,[status(thm)],[82,79]),
[iquote('0:MRR:82.3,79.3')] ).
cnf(109,plain,
( ~ one_sorted_str(skc16)
| rel_str(skc17) ),
inference(res,[status(thm),theory(equality)],[28,60]),
[iquote('0:Res:28.0,60.1')] ).
cnf(121,plain,
( ~ one_sorted_str(skc16)
| ~ net_str(skc17,skc16)
| subrelstr(skc18,skc17) ),
inference(res,[status(thm),theory(equality)],[36,90]),
[iquote('0:Res:36.0,90.1')] ).
cnf(138,plain,
( ~ rel_str(skc17)
| ~ subrelstr(u,skc17)
| ~ element(skc19,the_carrier(skc17))
| ~ element(skc20,the_carrier(skc17))
| ~ element(v,the_carrier(u))
| ~ equal(v,skc19)
| ~ related(u,v,skc20)
| ~ element(skc20,the_carrier(u)) ),
inference(res,[status(thm),theory(equality)],[85,41]),
[iquote('0:Res:85.8,41.0')] ).
cnf(139,plain,
rel_str(skc17),
inference(mrr,[status(thm)],[109,1]),
[iquote('0:MRR:109.0,1.0')] ).
cnf(142,plain,
subrelstr(skc18,skc17),
inference(mrr,[status(thm)],[121,1,28]),
[iquote('0:MRR:121.0,121.1,1.0,28.0')] ).
cnf(157,plain,
( ~ equal(u,skc19)
| ~ subrelstr(v,skc17)
| ~ element(u,the_carrier(v))
| ~ element(skc20,the_carrier(v))
| ~ related(v,u,skc20) ),
inference(mrr,[status(thm)],[138,139,35,34]),
[iquote('0:MRR:138.0,138.2,138.3,139.0,35.0,34.0')] ).
cnf(937,plain,
( ~ equal(skc19,skc19)
| ~ subrelstr(skc18,skc17)
| ~ element(skc19,the_carrier(skc18))
| ~ element(skc20,the_carrier(skc18)) ),
inference(res,[status(thm),theory(equality)],[86,157]),
[iquote('0:Res:86.0,157.4')] ).
cnf(938,plain,
( ~ subrelstr(skc18,skc17)
| ~ element(skc19,the_carrier(skc18))
| ~ element(skc20,the_carrier(skc18)) ),
inference(obv,[status(thm),theory(equality)],[937]),
[iquote('0:Obv:937.0')] ).
cnf(939,plain,
$false,
inference(mrr,[status(thm)],[938,142,87,38]),
[iquote('0:MRR:938.0,938.1,938.2,142.0,87.0,38.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU374+1 : TPTP v8.1.0. Released v3.3.0.
% 0.06/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n011.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 Jun 19 00:22:23 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.35/0.53
% 0.35/0.53 SPASS V 3.9
% 0.35/0.53 SPASS beiseite: Proof found.
% 0.35/0.53 % SZS status Theorem
% 0.35/0.53 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/0.53 SPASS derived 706 clauses, backtracked 0 clauses, performed 0 splits and kept 455 clauses.
% 0.35/0.53 SPASS allocated 98487 KBytes.
% 0.35/0.53 SPASS spent 0:00:00.17 on the problem.
% 0.35/0.53 0:00:00.04 for the input.
% 0.35/0.53 0:00:00.03 for the FLOTTER CNF translation.
% 0.35/0.53 0:00:00.01 for inferences.
% 0.35/0.53 0:00:00.00 for the backtracking.
% 0.35/0.53 0:00:00.05 for the reduction.
% 0.35/0.53
% 0.35/0.53
% 0.35/0.53 Here is a proof with depth 2, length 26 :
% 0.35/0.53 % SZS output start Refutation
% See solution above
% 0.35/0.53 Formulae used in the proof : t20_yellow_6 dt_l1_waybel_0 dt_m1_yellow_6 d8_yellow_6 t60_yellow_0
% 0.35/0.53
%------------------------------------------------------------------------------