%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN714-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n002.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:41:27 PM UTC 2026
% Result : Unsatisfiable 3.34s 11.50s
% Output : CNFRefutation 3.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of formulae : 37 ( 21 unt; 3 def)
% Number of atoms : 99 ( 3 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 72 ( 37 ~; 35 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 9 usr; 5 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 24 ( 0 sgn 24 !; 0 ?; 17 :)
% Comments :
%------------------------------------------------------------------------------
fof(f22,negated_conjecture,
p51(c66,c67),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p51_22) ).
fof(f23,negated_conjecture,
p53(c68,f17(c66)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p53_23) ).
fof(f24,negated_conjecture,
~ p16(f17(c66),c65),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p16_24) ).
fof(f28,negated_conjecture,
p52(f20(f21(c62,c64)),c66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p52_28) ).
fof(f33,negated_conjecture,
~ p50(c66,f25(f27(c59,c68),c67),c60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p50_33) ).
fof(f64,negated_conjecture,
! [X0] :
( ~ p53(X0,f17(c66))
| p50(c66,f25(f27(c59,X0),c67),c62) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p50_64) ).
fof(f87,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p53(X2,f17(X0))
| ~ p51(X0,X3)
| p51(X0,f25(f27(X1,X2),X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p51_87) ).
fof(f98,negated_conjecture,
! [X0,X1] :
( ~ p52(f20(f21(c62,c64)),X0)
| ~ p50(X0,X1,c62)
| ~ p51(X0,X1)
| p50(X0,X1,c60)
| p16(f17(X0),c65) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p16_98) ).
tcf(c_175,negated_conjecture,
p51(c66,c67),
inference(cnf_transformation,[],[f22]) ).
tcf(c_176,negated_conjecture,
p53(c68,f17(c66)),
inference(cnf_transformation,[],[f23]) ).
tcf(c_177,negated_conjecture,
~ p16(f17(c66),c65),
inference(cnf_transformation,[],[f24]) ).
tcf(c_181,negated_conjecture,
p52(f20(f21(c62,c64)),c66),
inference(cnf_transformation,[],[f28]) ).
tcf(c_186,negated_conjecture,
~ p50(c66,f25(f27(c59,c68),c67),c60),
inference(cnf_transformation,[],[f33]) ).
tcf(c_217,negated_conjecture,
! [X0: $i] :
( p50(c66,f25(f27(c59,X0),c67),c62)
| ~ p53(X0,f17(c66)) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_240,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p51(X1,f25(f27(X3,X0),X2))
| ~ p51(X1,X2)
| ~ p53(X0,f17(X1)) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_251,negated_conjecture,
! [X0: $i,X1: $i] :
( p16(f17(X0),c65)
| p50(X0,X1,c60)
| ~ p51(X0,X1)
| ~ p50(X0,X1,c62)
| ~ p52(f20(f21(c62,c64)),X0) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_1162,definition,
iPr_def_14 = f17(c66),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_1163,definition,
iPr_def_15 = f27(c59,c68),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_1164,definition,
iPr_def_16 = f25(iPr_def_15,c67),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_1171,negated_conjecture,
! [X0: $i,X1: $i] :
( p16(f17(X0),c65)
| p50(X0,X1,c60)
| ~ p52(iPr_def_13,X0)
| ~ p51(X0,X1)
| ~ p50(X0,X1,c62) ),
inference(demodulation,[status(thm)],[c_251]) ).
tcf(c_1179,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p51(X1,f25(f27(X3,X0),X2))
| ~ p51(X1,X2)
| ~ p53(X0,f17(X1)) ),
inference(demodulation,[status(thm)],[c_240]) ).
tcf(c_1188,negated_conjecture,
! [X0: $i] :
( p50(c66,f25(f27(c59,X0),c67),c62)
| ~ p53(X0,iPr_def_14) ),
inference(demodulation,[status(thm)],[c_217,c_1162]) ).
tcf(c_1203,negated_conjecture,
~ p50(c66,iPr_def_16,c60),
inference(demodulation,[status(thm)],[c_186,c_1163,c_1164]) ).
tcf(c_1205,negated_conjecture,
p52(iPr_def_13,c66),
inference(demodulation,[status(thm)],[c_181]) ).
tcf(c_1206,negated_conjecture,
~ p16(iPr_def_14,c65),
inference(demodulation,[status(thm)],[c_177]) ).
tcf(c_1207,negated_conjecture,
p53(c68,iPr_def_14),
inference(demodulation,[status(thm)],[c_176]) ).
tcf(c_1208,negated_conjecture,
p51(c66,c67),
inference(demodulation,[status(thm)],[c_175]) ).
tcf(c_2367,plain,
( p50(c66,f25(iPr_def_15,c67),c62)
| ~ p53(c68,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1163,c_1188]) ).
tcf(c_2368,plain,
( p50(c66,iPr_def_16,c62)
| ~ p53(c68,iPr_def_14) ),
inference(light_normalisation,[status(thm)],[c_2367,c_1164]) ).
tcf(c_2369,plain,
p50(c66,iPr_def_16,c62),
inference(forward_subsumption_resolution,[status(thm)],[c_2368,c_1207]) ).
tcf(c_2590,plain,
! [X0: $i,X1: $i] :
( p51(X0,f25(iPr_def_15,X1))
| ~ p51(X0,X1)
| ~ p53(c68,f17(X0)) ),
inference(superposition,[status(thm)],[c_1163,c_1179]) ).
tcf(c_2677,plain,
( p50(c66,iPr_def_16,c60)
| p16(f17(c66),c65)
| ~ p52(iPr_def_13,c66)
| ~ p51(c66,iPr_def_16) ),
inference(superposition,[status(thm)],[c_2369,c_1171]) ).
tcf(c_2678,plain,
( p16(iPr_def_14,c65)
| p50(c66,iPr_def_16,c60)
| ~ p52(iPr_def_13,c66)
| ~ p51(c66,iPr_def_16) ),
inference(light_normalisation,[status(thm)],[c_2677,c_1162]) ).
tcf(c_2679,plain,
~ p51(c66,iPr_def_16),
inference(forward_subsumption_resolution,[status(thm)],[c_2678,c_1206,c_1203,c_1205]) ).
tcf(c_5281,plain,
! [X0: $i] :
( p51(X0,iPr_def_16)
| ~ p51(X0,c67)
| ~ p53(c68,f17(X0)) ),
inference(superposition,[status(thm)],[c_1164,c_2590]) ).
tcf(c_5313,plain,
( p51(c66,iPr_def_16)
| ~ p53(c68,iPr_def_14)
| ~ p51(c66,c67) ),
inference(superposition,[status(thm)],[c_1162,c_5281]) ).
tcf(c_5314,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_5313,c_2679,c_1207,c_1208]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN714-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/10.59 % Computer : n002.cluster.edu
% 0.11/10.59 % Model : x86_64 x86_64
% 0.11/10.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.59 % Memory : 8046.5625MB
% 0.11/10.59 % OS : Linux 6.8.0-71-generic
% 0.11/10.59 % CPULimit : 300
% 0.11/10.59 % WCLimit : 300
% 0.11/10.59 % DateTime : Fri Sep 25 02:12:17 UTC 2026
% 0.11/10.59 % CPUTime :
% 0.11/10.59 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/10.63 Running first-order theorem proving
% 0.16/10.63 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.16/10.64
% 0.16/10.64 % ======== iProver multi-core TPTP/SMT =========
% 0.16/10.64
% 0.16/10.65 % Detected problem language: tptp
% 0.16/10.66 % Proving...
% 3.34/11.50 % SZS status Started for theBenchmark.p
% 3.34/11.50 % SZS status Unsatisfiable for theBenchmark.p
% 3.34/11.50
% 3.34/11.50 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.34/11.50
% 3.34/11.50 % ------ iProver source info
% 3.34/11.50
% 3.34/11.50 % git: date: 2026-07-19 20:42:38 +0200
% 3.34/11.50 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.34/11.50 % git: non_committed_changes: false
% 3.34/11.50
% 3.34/11.50 % ------ Parsing...% successful
% 3.34/11.50
% 3.34/11.50
% 3.34/11.50 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.34/11.50
% 3.34/11.50 % ------ Preprocessing... sf_s rm: 52 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 3.34/11.50
% 3.34/11.50 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.34/11.50
% 3.34/11.50 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 3.34/11.50 % ------ Proving...
% 3.34/11.50 % ------ Problem Properties
% 3.34/11.50
% 3.34/11.50 %
% 3.34/11.50 % clauses 61
% 3.34/11.50 % conjectures 53
% 3.34/11.50 % EPR 30
% 3.34/11.50 % Horn 52
% 3.34/11.50 % unary 24
% 3.34/11.50 % binary 5
% 3.34/11.50 % lits 152
% 3.34/11.50 % lits eq 8
% 3.34/11.50 % fd_pure 0
% 3.34/11.50 % fd_pseudo 0
% 3.34/11.50 % fd_cond 0
% 3.34/11.50 % fd_pseudo_cond 0
% 3.34/11.50 % AC symbols 0
% 3.34/11.50
% 3.34/11.50 % ------ Schedule dynamic 5 is on
% 3.34/11.50
% 3.34/11.50 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 3.34/11.50
% 3.34/11.50
% 3.34/11.50 % ------
% 3.34/11.50 % Current options:
% 3.34/11.50 % ------
% 3.34/11.50
% 3.34/11.50
% 3.34/11.50 %
% 3.34/11.50
% 3.34/11.50 % ------ Proving...
% 3.34/11.50 %
% 3.34/11.50
% 3.34/11.50 % SZS status Unsatisfiable for theBenchmark.p
% 3.34/11.50
% 3.34/11.50 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.34/11.50
% 3.34/11.50
%------------------------------------------------------------------------------