%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL118-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n014.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 : Fri Sep 25 02:05:43 PM UTC 2026
% Result : Unsatisfiable 7.22s 11.79s
% Output : CNFRefutation 7.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 3
% Syntax : Number of formulae : 73 ( 18 unt; 0 def)
% Number of atoms : 159 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 222 ( 136 ~; 86 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 156 ( 0 sgn 156 !; 0 ?; 151 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X2,equivalent(X1,X0)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wo) ).
fof(f3,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(a,b),equivalent(equivalent(c,b),equivalent(c,a)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_yqm) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X2,equivalent(X1,X0)))),
inference(cnf_transformation,[],[f2]) ).
tcf(c_54,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(a,b),equivalent(equivalent(c,b),equivalent(c,a)))),
inference(cnf_transformation,[],[f3]) ).
tcf(c_71,plain,
! [X0: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(a,b),equivalent(equivalent(c,b),equivalent(c,a))))) ),
inference(resolution,[status(thm)],[c_52,c_54]) ).
tcf(c_77,plain,
~ is_a_theorem(equivalent(equivalent(c,a),equivalent(equivalent(c,b),equivalent(a,b)))),
inference(resolution,[status(thm)],[c_71,c_53]) ).
tcf(c_85,plain,
! [X0: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(c,a),equivalent(equivalent(c,b),equivalent(a,b))))) ),
inference(resolution,[status(thm)],[c_77,c_52]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(c,a),equivalent(equivalent(c,b),equivalent(a,b)))))) ),
inference(resolution,[status(thm)],[c_85,c_52]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,equivalent(X1,X0)))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,equivalent(X1,equivalent(X0,X2))))),
inference(superposition,[status(thm)],[c_53,c_92]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,equivalent(X1,equivalent(X0,X2))))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_93,c_52]) ).
tcf(c_122,plain,
! [X0: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(equivalent(c,b),equivalent(a,b)),equivalent(equivalent(c,a),X0))) ),
inference(resolution,[status(thm)],[c_89,c_53]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X2),equivalent(X1,X2)))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_110,c_92]) ).
tcf(c_137,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(c,b),equivalent(a,b)),equivalent(equivalent(c,a),X1)))) ),
inference(resolution,[status(thm)],[c_122,c_52]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(equivalent(c,b),equivalent(a,b)),equivalent(equivalent(c,a),X2))))) ),
inference(resolution,[status(thm)],[c_137,c_52]) ).
tcf(c_159,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,equivalent(X1,X0)))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(equivalent(X0,X2))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_125,c_52]) ).
tcf(c_162,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,equivalent(X1,equivalent(X0,X2))))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_125,c_159]) ).
tcf(c_211,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(X2,equivalent(X1,X0)),X3))
| ~ is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),X3)) ),
inference(superposition,[status(thm)],[c_53,c_160]) ).
tcf(c_213,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( is_a_theorem(equivalent(equivalent(X1,equivalent(X0,X2)),X3))
| ~ is_a_theorem(equivalent(X2,X3))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_162,c_160]) ).
tcf(c_217,plain,
( is_a_theorem(equivalent(equivalent(a,equivalent(a,a)),a))
| ~ is_a_theorem(equivalent(a,a)) ),
inference(instantiation,[status(thm)],[c_213]) ).
tcf(c_504,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(equivalent(c,a),X0),equivalent(equivalent(equivalent(c,b),equivalent(a,b)),X1))) ),
inference(resolution,[status(thm)],[c_148,c_53]) ).
tcf(c_520,plain,
! [X0: $i] :
( ~ is_a_theorem(equivalent(X0,equivalent(c,a)))
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(c,b),equivalent(a,b)))) ),
inference(resolution,[status(thm)],[c_504,c_53]) ).
tcf(c_526,plain,
~ is_a_theorem(equivalent(equivalent(b,equivalent(a,equivalent(c,b))),equivalent(c,a))),
inference(resolution,[status(thm)],[c_520,c_53]) ).
tcf(c_528,plain,
! [X0: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(b,equivalent(a,equivalent(c,b))),equivalent(c,a)))) ),
inference(resolution,[status(thm)],[c_526,c_52]) ).
tcf(c_532,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(b,equivalent(a,equivalent(c,b))),equivalent(c,a))))) ),
inference(resolution,[status(thm)],[c_528,c_52]) ).
tcf(c_581,plain,
! [X0: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(c,a),equivalent(equivalent(b,equivalent(a,equivalent(c,b))),X0))) ),
inference(resolution,[status(thm)],[c_532,c_53]) ).
tcf(c_585,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(c,a),equivalent(equivalent(b,equivalent(a,equivalent(c,b))),X1)))) ),
inference(resolution,[status(thm)],[c_581,c_52]) ).
tcf(c_635,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(c,a),equivalent(equivalent(b,equivalent(a,equivalent(c,b))),X2))))) ),
inference(resolution,[status(thm)],[c_585,c_52]) ).
tcf(c_1604,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,equivalent(X1,X0)))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_1625,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X0,equivalent(X1,X2)))),
inference(superposition,[status(thm)],[c_53,c_211]) ).
tcf(c_1653,plain,
! [X0: $i,X1: $i,X2: $i] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,equivalent(X2,equivalent(X0,X1))))),
inference(superposition,[status(thm)],[c_1625,c_1604]) ).
tcf(c_1657,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,equivalent(X2,equivalent(X0,X1))))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_1653,c_52]) ).
tcf(c_1663,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,X2)))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_1657,c_1604]) ).
tcf(c_1667,plain,
! [X0: $i,X1: $i,X2: $i] :
( is_a_theorem(equivalent(X2,X2))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(superposition,[status(thm)],[c_1663,c_52]) ).
tcf(c_1680,plain,
! [X0: $i] : is_a_theorem(equivalent(X0,X0)),
inference(superposition,[status(thm)],[c_1653,c_1667]) ).
tcf(c_1683,plain,
is_a_theorem(equivalent(a,a)),
inference(instantiation,[status(thm)],[c_1680]) ).
tcf(c_2033,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(equivalent(b,equivalent(a,equivalent(c,b))),X0),equivalent(equivalent(c,a),X1))) ),
inference(resolution,[status(thm)],[c_635,c_53]) ).
tcf(c_2040,plain,
! [X0: $i] :
( ~ is_a_theorem(equivalent(X0,equivalent(c,a)))
| ~ is_a_theorem(equivalent(X0,equivalent(b,equivalent(a,equivalent(c,b))))) ),
inference(resolution,[status(thm)],[c_2033,c_53]) ).
tcf(c_2044,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X1,equivalent(c,a)))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(b,equivalent(a,equivalent(c,b)))))) ),
inference(resolution,[status(thm)],[c_2040,c_52]) ).
tcf(c_2098,plain,
! [X0: $i] :
( ~ is_a_theorem(equivalent(X0,equivalent(c,a)))
| ~ is_a_theorem(equivalent(equivalent(a,equivalent(c,b)),equivalent(b,X0))) ),
inference(resolution,[status(thm)],[c_2044,c_53]) ).
tcf(c_2103,plain,
~ is_a_theorem(equivalent(equivalent(c,a),equivalent(c,a))),
inference(resolution,[status(thm)],[c_2098,c_53]) ).
tcf(c_2105,plain,
! [X0: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(c,a),equivalent(c,a)))) ),
inference(resolution,[status(thm)],[c_2103,c_52]) ).
tcf(c_2109,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(c,a),equivalent(c,a))))) ),
inference(resolution,[status(thm)],[c_2105,c_52]) ).
tcf(c_2208,plain,
! [X0: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(c,a),equivalent(equivalent(c,a),X0))) ),
inference(resolution,[status(thm)],[c_2109,c_53]) ).
tcf(c_2212,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(c,a),equivalent(equivalent(c,a),X1)))) ),
inference(resolution,[status(thm)],[c_2208,c_52]) ).
tcf(c_2290,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_a_theorem(X2)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(c,a),equivalent(equivalent(c,a),X2))))) ),
inference(resolution,[status(thm)],[c_2212,c_52]) ).
tcf(c_4700,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(equivalent(c,a),X0),equivalent(equivalent(c,a),X1))) ),
inference(resolution,[status(thm)],[c_2290,c_53]) ).
tcf(c_4707,plain,
! [X0: $i] : ~ is_a_theorem(equivalent(X0,equivalent(c,a))),
inference(resolution,[status(thm)],[c_4700,c_53]) ).
tcf(c_4717,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(c,a)))) ),
inference(resolution,[status(thm)],[c_4707,c_52]) ).
tcf(c_4721,plain,
! [X0: $i] : ~ is_a_theorem(equivalent(a,equivalent(c,X0))),
inference(resolution,[status(thm)],[c_4717,c_53]) ).
tcf(c_4723,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(c,X1)))) ),
inference(resolution,[status(thm)],[c_4721,c_52]) ).
tcf(c_4726,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(a,equivalent(c,X2))))) ),
inference(resolution,[status(thm)],[c_4723,c_52]) ).
tcf(c_4740,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(equivalent(c,X0),equivalent(a,X1))) ),
inference(resolution,[status(thm)],[c_4726,c_53]) ).
tcf(c_4743,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_a_theorem(X2)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(c,X1),equivalent(a,X2)))) ),
inference(resolution,[status(thm)],[c_4740,c_52]) ).
tcf(c_4753,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ is_a_theorem(X3)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(c,X2),equivalent(a,X3))))) ),
inference(resolution,[status(thm)],[c_4743,c_52]) ).
tcf(c_6197,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_a_theorem(X2)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(equivalent(a,X0),equivalent(equivalent(c,X1),X2))) ),
inference(resolution,[status(thm)],[c_4753,c_53]) ).
tcf(c_6202,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(equivalent(X0,a))
| ~ is_a_theorem(equivalent(X0,equivalent(c,X1))) ),
inference(resolution,[status(thm)],[c_6197,c_53]) ).
tcf(c_6205,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X1,a))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(c,X2)))) ),
inference(resolution,[status(thm)],[c_6202,c_52]) ).
tcf(c_6217,plain,
! [X0: $i,X1: $i] :
( ~ is_a_theorem(equivalent(X1,a))
| ~ is_a_theorem(equivalent(X0,equivalent(c,X1))) ),
inference(resolution,[status(thm)],[c_6205,c_53]) ).
tcf(c_6221,plain,
! [X0: $i,X1: $i] : ~ is_a_theorem(equivalent(equivalent(X0,X1),a)),
inference(resolution,[status(thm)],[c_6217,c_53]) ).
tcf(c_6224,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),a))) ),
inference(resolution,[status(thm)],[c_6221,c_52]) ).
tcf(c_6227,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(X2,X3),a)))) ),
inference(resolution,[status(thm)],[c_6224,c_52]) ).
tcf(c_6245,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(a,equivalent(equivalent(X0,X1),X2))) ),
inference(resolution,[status(thm)],[c_6227,c_53]) ).
tcf(c_6248,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ is_a_theorem(X3)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(a,equivalent(equivalent(X1,X2),X3)))) ),
inference(resolution,[status(thm)],[c_6245,c_52]) ).
tcf(c_6257,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ is_a_theorem(X4)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,equivalent(X1,equivalent(a,equivalent(equivalent(X2,X3),X4))))) ),
inference(resolution,[status(thm)],[c_6248,c_52]) ).
tcf(c_6857,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ is_a_theorem(X3)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X2),equivalent(a,X3))) ),
inference(resolution,[status(thm)],[c_6257,c_53]) ).
tcf(c_6863,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ is_a_theorem(equivalent(X0,a))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(resolution,[status(thm)],[c_6857,c_53]) ).
tcf(c_6868,plain,
! [X0: $i,X1: $i,X2: $i] : ~ is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),a)),
inference(resolution,[status(thm)],[c_6863,c_53]) ).
tcf(c_6869,plain,
~ is_a_theorem(equivalent(equivalent(a,equivalent(a,a)),a)),
inference(instantiation,[status(thm)],[c_6868]) ).
tcf(c_6870,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_6869,c_1683,c_217]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL118-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/10.39 % Computer : n014.cluster.edu
% 0.11/10.39 % Model : x86_64 x86_64
% 0.11/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.39 % Memory : 8046.5625MB
% 0.11/10.39 % OS : Linux 6.8.0-71-generic
% 0.11/10.40 % CPULimit : 300
% 0.11/10.40 % WCLimit : 300
% 0.11/10.40 % DateTime : Wed Sep 23 21:59:58 UTC 2026
% 0.15/10.40 % CPUTime :
% 0.15/10.40 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/10.44 Running first-order theorem proving
% 0.15/10.44 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/10.45
% 0.15/10.45 % ======== iProver multi-core TPTP/SMT =========
% 0.15/10.45
% 0.15/10.45 % Detected problem language: tptp
% 0.15/10.46 % Proving...
% 7.22/11.79 % SZS status Started for theBenchmark.p
% 7.22/11.79 % SZS status Unsatisfiable for theBenchmark.p
% 7.22/11.79
% 7.22/11.79 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.22/11.79
% 7.22/11.79 % ------ iProver source info
% 7.22/11.79
% 7.22/11.79 % git: date: 2026-07-19 20:42:38 +0200
% 7.22/11.79 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.22/11.79 % git: non_committed_changes: false
% 7.22/11.79
% 7.22/11.79 % ------ Parsing...% successful
% 7.22/11.79
% 7.22/11.79
% 7.22/11.79 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 7.22/11.79
% 7.22/11.79 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 7.22/11.79
% 7.22/11.79 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 7.22/11.79 % ------ Proving...
% 7.22/11.79 % ------ Problem Properties
% 7.22/11.79
% 7.22/11.79 %
% 7.22/11.79 % clauses 3
% 7.22/11.79 % conjectures 1
% 7.22/11.79 % EPR 0
% 7.22/11.79 % Horn 3
% 7.22/11.79 % unary 2
% 7.22/11.79 % binary 0
% 7.22/11.79 % lits 5
% 7.22/11.79 % lits eq 0
% 7.22/11.79 % fd_pure 0
% 7.22/11.79 % fd_pseudo 0
% 7.22/11.79 % fd_cond 0
% 7.22/11.79 % fd_pseudo_cond 0
% 7.22/11.79 % AC symbols 0
% 7.22/11.79
% 7.22/11.79 % ------ Input Options Time Limit: Unbounded
% 7.22/11.79
% 7.22/11.79
% 7.22/11.79 % ------
% 7.22/11.79 % Current options:
% 7.22/11.79 % ------
% 7.22/11.79
% 7.22/11.79
% 7.22/11.79 %
% 7.22/11.79
% 7.22/11.79 % ------ Proving...
% 7.22/11.79 %
% 7.22/11.79
% 7.22/11.79 % SZS status Unsatisfiable for theBenchmark.p
% 7.22/11.79
% 7.22/11.79 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 7.22/11.79
% 7.22/11.79
%------------------------------------------------------------------------------