%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN098-1.002 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n012.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 03:39:11 PM UTC 2026
% Result : Unsatisfiable 0.65s 1.06s
% Output : CNFRefutation 0.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 16
% Syntax : Number of formulae : 33 ( 3 unt; 0 def)
% Number of atoms : 81 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 92 ( 44 ~; 48 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 15 usr; 16 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
fof(f35,axiom,
( sym_q_0
| sym_p_0
| ~ sym_u_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_s3_goal_1) ).
fof(f36,axiom,
sym_u_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_1_s3_goal_1) ).
fof(f39,axiom,
( sym_q_2
| sym_q_1
| ~ sym_p_0
| ~ sym_u_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_s3_type11_2) ).
fof(f40,axiom,
( sym_u_3
| ~ sym_p_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_3_s3_type11_2) ).
fof(f43,axiom,
( sym_q_3
| sym_q_2
| ~ sym_p_1
| ~ sym_u_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_s3_type11_4) ).
fof(f44,axiom,
( sym_u_5
| ~ sym_p_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_5_s3_type11_4) ).
fof(f45,axiom,
( sym_q_2
| sym_p_1
| ~ sym_q_0
| ~ sym_u_6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_s3_type12_1) ).
fof(f46,axiom,
( sym_u_6
| ~ sym_q_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_6_s3_type12_1) ).
fof(f49,axiom,
( sym_q_3
| sym_p_2
| ~ sym_q_1
| ~ sym_u_8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_s3_type12_3) ).
fof(f50,axiom,
( sym_u_8
| ~ sym_q_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_8_s3_type12_3) ).
fof(f61,axiom,
( ~ sym_p_2
| ~ sym_u_14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_t3_1) ).
fof(f62,axiom,
( sym_u_14
| ~ sym_p_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_14_t3_1) ).
fof(f65,axiom,
( ~ sym_q_2
| ~ sym_u_16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_t3_3) ).
fof(f66,axiom,
( sym_u_16
| ~ sym_q_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_16_t3_3) ).
fof(f67,axiom,
( ~ sym_q_3
| ~ sym_u_17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_t3_4) ).
fof(f68,axiom,
( sym_u_17
| ~ sym_q_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sym_u_17_t3_4) ).
tcf(c_147,plain,
( sym_q_0
| sym_p_0
| ~ sym_u_1 ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_148,plain,
sym_u_1,
inference(cnf_transformation,[],[f36]) ).
tcf(c_151,plain,
( sym_q_2
| sym_q_1
| ~ sym_u_3
| ~ sym_p_0 ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_152,plain,
( sym_u_3
| ~ sym_p_0 ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_155,plain,
( sym_q_3
| sym_q_2
| ~ sym_u_5
| ~ sym_p_1 ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_156,plain,
( sym_u_5
| ~ sym_p_1 ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_157,plain,
( sym_q_2
| sym_p_1
| ~ sym_u_6
| ~ sym_q_0 ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_158,plain,
( sym_u_6
| ~ sym_q_0 ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_161,plain,
( sym_q_3
| sym_p_2
| ~ sym_u_8
| ~ sym_q_1 ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_162,plain,
( sym_u_8
| ~ sym_q_1 ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_169,plain,
( ~ sym_u_14
| ~ sym_p_2 ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_170,plain,
( sym_u_14
| ~ sym_p_2 ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_173,plain,
( ~ sym_u_16
| ~ sym_q_2 ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_174,plain,
( sym_u_16
| ~ sym_q_2 ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_175,plain,
( ~ sym_u_17
| ~ sym_q_3 ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_176,plain,
( sym_u_17
| ~ sym_q_3 ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_177,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_151,c_155,c_157,c_161,c_147,c_169,c_173,c_175,c_152,c_156,c_158,c_162,c_170,c_174,c_176,c_148]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN098-1.002 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.05/0.30 % Computer : n012.cluster.edu
% 0.05/0.30 % Model : x86_64 x86_64
% 0.05/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.30 % Memory : 8046.5625MB
% 0.05/0.30 % OS : Linux 6.8.0-71-generic
% 0.05/0.30 % CPULimit : 300
% 0.05/0.30 % WCLimit : 300
% 0.05/0.30 % DateTime : Fri Sep 25 00:09:36 UTC 2026
% 0.05/0.30 % CPUTime :
% 0.05/0.30 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.05/0.32 Running first-order theorem proving
% 0.05/0.32 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.06/0.33
% 0.06/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.06/0.33
% 0.06/0.33 % Detected problem language: tptp
% 0.06/0.33 % Proving...
% 0.65/1.06 % SZS status Started for theBenchmark.p
% 0.65/1.06 % SZS status Unsatisfiable for theBenchmark.p
% 0.65/1.06
% 0.65/1.06 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 0.65/1.06
% 0.65/1.06 % ------ iProver source info
% 0.65/1.06
% 0.65/1.06 % git: date: 2026-07-19 20:42:38 +0200
% 0.65/1.06 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 0.65/1.06 % git: non_committed_changes: false
% 0.65/1.06
% 0.65/1.06 % ------ Parsing...% successful
% 0.65/1.06
% 0.65/1.06
% 0.65/1.06 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 0.65/1.06 %
% 0.65/1.06
% 0.65/1.06 % ------ Preprocessing...%
% 0.65/1.06
% 0.65/1.06 % SZS status Unsatisfiable for theBenchmark.p
% 0.65/1.06
% 0.65/1.06 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 0.65/1.06
% 0.65/1.06
%------------------------------------------------------------------------------