%------------------------------------------------------------------------------
% File : SPASS+T---2.2.22
% Problem : TIM031_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : spasst-tptp-script %s %d
% Computer : n013.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:17:40 PM UTC 2026
% Result : Theorem 0.77s 1.03s
% Output : CNFRefutation 0.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 17
% Syntax : Number of clauses : 41 ( 22 unt; 0 nHn; 41 RR)
% Number of literals : 88 ( 0 equ; 51 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 15 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
interval(h),
file('TIM031_1.p',unknown),
[] ).
cnf(2,axiom,
interval(g),
file('TIM031_1.p',unknown),
[] ).
cnf(3,axiom,
interval(f),
file('TIM031_1.p',unknown),
[] ).
cnf(4,axiom,
interval(e),
file('TIM031_1.p',unknown),
[] ).
cnf(5,axiom,
interval(d),
file('TIM031_1.p',unknown),
[] ).
cnf(6,axiom,
interval(c),
file('TIM031_1.p',unknown),
[] ).
cnf(7,axiom,
interval(b),
file('TIM031_1.p',unknown),
[] ).
cnf(8,axiom,
interval(a),
file('TIM031_1.p',unknown),
[] ).
cnf(10,axiom,
before(g,h),
file('TIM031_1.p',unknown),
[] ).
cnf(11,axiom,
before(f,g),
file('TIM031_1.p',unknown),
[] ).
cnf(12,axiom,
before(e,f),
file('TIM031_1.p',unknown),
[] ).
cnf(13,axiom,
before(d,e),
file('TIM031_1.p',unknown),
[] ).
cnf(14,axiom,
before(c,d),
file('TIM031_1.p',unknown),
[] ).
cnf(15,axiom,
before(b,c),
file('TIM031_1.p',unknown),
[] ).
cnf(16,axiom,
before(a,b),
file('TIM031_1.p',unknown),
[] ).
cnf(17,axiom,
~ before(a,h),
file('TIM031_1.p',unknown),
[] ).
cnf(31,axiom,
( ~ interval(U)
| ~ interval(V)
| ~ interval(W)
| ~ before(U,V)
| ~ before(V,W)
| before(U,W) ),
file('TIM031_1.p',unknown),
[] ).
cnf(33,plain,
( ~ interval(h)
| ~ interval(U)
| ~ before(U,h)
| ~ before(a,U)
| ~ interval(a) ),
inference(res,[status(thm),theory(equality)],[31,17]),
[iquote('0:Res:31.5,17.0')] ).
cnf(35,plain,
( ~ interval(U)
| ~ before(U,h)
| ~ before(a,U) ),
inference(mrr,[status(thm)],[33,1,8]),
[iquote('0:MRR:33.0,33.4,1.0,8.0')] ).
cnf(67,plain,
( ~ interval(a)
| ~ interval(b)
| ~ interval(U)
| ~ before(b,U)
| before(a,U) ),
inference(res,[status(thm),theory(equality)],[16,31]),
[iquote('0:Res:16.0,31.3')] ).
cnf(68,plain,
( ~ interval(b)
| ~ interval(c)
| ~ interval(U)
| ~ before(c,U)
| before(b,U) ),
inference(res,[status(thm),theory(equality)],[15,31]),
[iquote('0:Res:15.0,31.3')] ).
cnf(69,plain,
( ~ interval(c)
| ~ interval(d)
| ~ interval(U)
| ~ before(d,U)
| before(c,U) ),
inference(res,[status(thm),theory(equality)],[14,31]),
[iquote('0:Res:14.0,31.3')] ).
cnf(70,plain,
( ~ interval(d)
| ~ interval(e)
| ~ interval(U)
| ~ before(e,U)
| before(d,U) ),
inference(res,[status(thm),theory(equality)],[13,31]),
[iquote('0:Res:13.0,31.3')] ).
cnf(72,plain,
( ~ interval(f)
| ~ interval(g)
| ~ interval(U)
| ~ before(g,U)
| before(f,U) ),
inference(res,[status(thm),theory(equality)],[11,31]),
[iquote('0:Res:11.0,31.3')] ).
cnf(74,plain,
( ~ interval(U)
| ~ before(b,U)
| before(a,U) ),
inference(mrr,[status(thm)],[67,8,7]),
[iquote('0:MRR:67.0,67.1,8.0,7.0')] ).
cnf(75,plain,
( ~ interval(U)
| ~ before(c,U)
| before(b,U) ),
inference(mrr,[status(thm)],[68,7,6]),
[iquote('0:MRR:68.0,68.1,7.0,6.0')] ).
cnf(76,plain,
( ~ interval(U)
| ~ before(d,U)
| before(c,U) ),
inference(mrr,[status(thm)],[69,6,5]),
[iquote('0:MRR:69.0,69.1,6.0,5.0')] ).
cnf(77,plain,
( ~ interval(U)
| ~ before(e,U)
| before(d,U) ),
inference(mrr,[status(thm)],[70,5,4]),
[iquote('0:MRR:70.0,70.1,5.0,4.0')] ).
cnf(79,plain,
( ~ interval(U)
| ~ before(g,U)
| before(f,U) ),
inference(mrr,[status(thm)],[72,3,2]),
[iquote('0:MRR:72.0,72.1,3.0,2.0')] ).
cnf(122,plain,
( ~ interval(f)
| before(d,f) ),
inference(res,[status(thm),theory(equality)],[12,77]),
[iquote('0:Res:12.0,77.1')] ).
cnf(123,plain,
before(d,f),
inference(mrr,[status(thm)],[122,3]),
[iquote('0:MRR:122.0,3.0')] ).
cnf(126,plain,
( ~ interval(f)
| before(c,f) ),
inference(res,[status(thm),theory(equality)],[123,76]),
[iquote('0:Res:123.0,76.1')] ).
cnf(129,plain,
before(c,f),
inference(mrr,[status(thm)],[126,3]),
[iquote('0:MRR:126.0,3.0')] ).
cnf(132,plain,
( ~ interval(f)
| before(b,f) ),
inference(res,[status(thm),theory(equality)],[129,75]),
[iquote('0:Res:129.0,75.1')] ).
cnf(135,plain,
before(b,f),
inference(mrr,[status(thm)],[132,3]),
[iquote('0:MRR:132.0,3.0')] ).
cnf(141,plain,
( ~ interval(f)
| before(a,f) ),
inference(res,[status(thm),theory(equality)],[135,74]),
[iquote('0:Res:135.0,74.1')] ).
cnf(144,plain,
before(a,f),
inference(mrr,[status(thm)],[141,3]),
[iquote('0:MRR:141.0,3.0')] ).
cnf(154,plain,
( ~ interval(h)
| before(f,h) ),
inference(res,[status(thm),theory(equality)],[10,79]),
[iquote('0:Res:10.0,79.1')] ).
cnf(155,plain,
before(f,h),
inference(mrr,[status(thm)],[154,1]),
[iquote('0:MRR:154.0,1.0')] ).
cnf(168,plain,
( ~ interval(f)
| ~ before(a,f) ),
inference(res,[status(thm),theory(equality)],[155,35]),
[iquote('0:Res:155.0,35.1')] ).
cnf(173,plain,
$false,
inference(mrr,[status(thm)],[168,3,144]),
[iquote('0:MRR:168.0,168.1,3.0,144.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : TIM031_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : spasst-tptp-script %s %d
% 0.17/0.33 % Computer : n013.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.33 % CPULimit : 300
% 0.17/0.33 % WCLimit : 300
% 0.17/0.33 % DateTime : Mon May 4 18:29:25 EDT 2026
% 0.17/0.33 % CPUTime :
% 0.32/0.46 % Using EUF theory
% 0.77/1.03
% 0.77/1.03
% 0.77/1.03 % SZS status Theorem for /tmp/SPASST_31025_n013.cluster.edu
% 0.77/1.03
% 0.77/1.03 SPASS V 2.2.22 in combination with yices.
% 0.77/1.03 SPASS beiseite: Proof found by SPASS.
% 0.77/1.03 Problem: /tmp/SPASST_31025_n013.cluster.edu
% 0.77/1.03 SPASS derived 76 clauses, backtracked 0 clauses and kept 90 clauses.
% 0.77/1.03 SPASS backtracked 0 times (0 times due to theory inconsistency).
% 0.77/1.03 SPASS allocated 6383 KBytes.
% 0.77/1.03 SPASS spent 0:00:00.02 on the problem.
% 0.77/1.03 0:00:00.00 for the input.
% 0.77/1.03 0:00:00.00 for the FLOTTER CNF translation.
% 0.77/1.03 0:00:00.00 for inferences.
% 0.77/1.03 0:00:00.00 for the backtracking.
% 0.77/1.03 0:00:00.00 for the reduction.
% 0.77/1.03 0:00:00.00 for interacting with the SMT procedure.
% 0.77/1.03
% 0.77/1.03
% 0.77/1.03 % SZS output start CNFRefutation for /tmp/SPASST_31025_n013.cluster.edu
% See solution above
% 0.77/1.03
% 0.77/1.03 Formulae used in the proof : fof_h fof_g fof_f fof_e fof_d fof_c fof_b fof_a fof_p7 fof_p6 fof_p5 fof_p4 fof_p3 fof_p2 fof_p1 fof_goal fof_before_transitive
% 0.77/1.05
% 0.77/1.05 SPASS+T ended
%------------------------------------------------------------------------------