%------------------------------------------------------------------------------
% File : SPASS+T---2.2.22
% Problem : SWX000_1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : spasst-tptp-script %s %d
% Computer : n029.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 : Sun Apr 6 10:09:27 AM UTC 2025
% Result : Theorem 0.86s 1.12s
% Output : Refutation 0.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 9
% Syntax : Number of clauses : 22 ( 9 unt; 3 nHn; 18 RR)
% Number of literals : 47 ( 0 equ; 26 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 10 ( 3 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(6,axiom,
general(skc4),
file('SWX000_1.p',unknown),
[] ).
cnf(10,axiom,
( tq(U)
| skP0(V,U) ),
file('SWX000_1.p',unknown),
[] ).
cnf(11,axiom,
( hp(U)
| skP0(U,V) ),
file('SWX000_1.p',unknown),
[] ).
cnf(14,axiom,
( ~ skP0(skc4,skc5)
| tq(skc5) ),
file('SWX000_1.p',unknown),
[] ).
cnf(16,axiom,
( ~ hq(U)
| skP0(V,U) ),
file('SWX000_1.p',unknown),
[] ).
cnf(17,axiom,
( equal(U,V)
| skP0(V,U) ),
file('SWX000_1.p',unknown),
[] ).
cnf(19,axiom,
( ~ tq(skc5)
| ~ skP0(skc4,skc5) ),
file('SWX000_1.p',unknown),
[] ).
cnf(20,axiom,
( ~ skP0(skc4,skc5)
| equal(skc5,skc4) ),
file('SWX000_1.p',unknown),
[] ).
cnf(45,axiom,
( ~ general(U)
| ~ hp(V)
| ~ tq(V)
| ~ general(V)
| ~ equal(U,V)
| hq(U) ),
file('SWX000_1.p',unknown),
[] ).
cnf(48,plain,
tq(skc5),
inference(mrr,[status(thm)],[14,10]),
[iquote('0:MRR:14.0,10.0')] ).
cnf(49,plain,
equal(skc5,skc4),
inference(mrr,[status(thm)],[20,17]),
[iquote('0:MRR:20.0,17.0')] ).
cnf(52,plain,
tq(skc4),
inference(rew,[status(thm),theory(equality)],[49,48]),
[iquote('0:Rew:49.0,48.0')] ).
cnf(53,plain,
( ~ tq(skc4)
| ~ skP0(skc4,skc4) ),
inference(rew,[status(thm),theory(equality)],[49,19]),
[iquote('0:Rew:49.0,19.1,49.0,19.0')] ).
cnf(54,plain,
~ skP0(skc4,skc4),
inference(mrr,[status(thm)],[53,52]),
[iquote('0:MRR:53.0,52.0')] ).
cnf(91,plain,
( ~ general(skc4)
| ~ tq(skc4)
| ~ hp(skc4)
| ~ general(skc5)
| hq(skc5) ),
inference(res,[status(thm),theory(equality)],[49,45]),
[iquote('0:Res:49.0,45.3')] ).
cnf(117,plain,
( ~ general(skc4)
| ~ tq(skc4)
| ~ hp(skc4)
| ~ general(skc4)
| hq(skc4) ),
inference(rew,[status(thm),theory(equality)],[49,91]),
[iquote('0:Rew:49.0,91.4,49.0,91.3')] ).
cnf(118,plain,
( ~ tq(skc4)
| ~ hp(skc4)
| ~ general(skc4)
| hq(skc4) ),
inference(obv,[status(thm),theory(equality)],[117]),
[iquote('0:Obv:117.0')] ).
cnf(119,plain,
( ~ hp(skc4)
| hq(skc4) ),
inference(mrr,[status(thm)],[118,52,6]),
[iquote('0:MRR:118.0,118.2,52.0,6.0')] ).
cnf(209,plain,
hp(skc4),
inference(res,[status(thm),theory(equality)],[11,54]),
[iquote('0:Res:11.1,54.0')] ).
cnf(210,plain,
~ hq(skc4),
inference(res,[status(thm),theory(equality)],[16,54]),
[iquote('0:Res:16.1,54.0')] ).
cnf(213,plain,
hq(skc4),
inference(mrr,[status(thm)],[119,209]),
[iquote('0:MRR:119.0,209.0')] ).
cnf(216,plain,
$false,
inference(mrr,[status(thm)],[210,213]),
[iquote('0:MRR:210.0,213.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWX000_1 : TPTP v9.1.0. Released v9.1.0.
% 0.07/0.13 % Command : spasst-tptp-script %s %d
% 0.13/0.34 % Computer : n029.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Sun Apr 6 03:07:19 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.20/0.48 % Using EUF theory
% 0.86/1.12
% 0.86/1.12
% 0.86/1.12 % SZS status Theorem for /tmp/SPASST_7352_n029.cluster.edu
% 0.86/1.12
% 0.86/1.12 SPASS V 2.2.22 in combination with yices.
% 0.86/1.12 SPASS beiseite: Proof found by SPASS.
% 0.86/1.12 Problem: /tmp/SPASST_7352_n029.cluster.edu
% 0.86/1.12 SPASS derived 109 clauses, backtracked 38 clauses and kept 170 clauses.
% 0.86/1.12 SPASS backtracked 2 times (0 times due to theory inconsistency).
% 0.86/1.12 SPASS allocated 6424 KBytes.
% 0.86/1.12 SPASS spent 0:00:00.02 on the problem.
% 0.86/1.12 0:00:00.00 for the input.
% 0.86/1.12 0:00:00.01 for the FLOTTER CNF translation.
% 0.86/1.12 0:00:00.00 for inferences.
% 0.86/1.12 0:00:00.00 for the backtracking.
% 0.86/1.12 0:00:00.01 for the reduction.
% 0.86/1.12 0:00:00.00 for interacting with the SMT procedure.
% 0.86/1.12
% 0.86/1.12
% 0.86/1.12 % SZS output start CNFRefutation for /tmp/SPASST_7352_n029.cluster.edu
% See solution above
% 0.86/1.12
% 0.86/1.12 Formulae used in the proof : fof_formula_3_left_0 fof_formula_2_right_0
% 0.86/1.14
% 0.86/1.14 SPASS+T ended
%------------------------------------------------------------------------------