%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ROB014-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n018.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:39:43 PM UTC 2026
% Result : Unsatisfiable 10.31s 2.27s
% Output : CNFRefutation 10.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 12
% Syntax : Number of formulae : 76 ( 76 unt; 6 def)
% Number of atoms : 228 ( 75 equ)
% Maximal formula atoms : 1 ( 3 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 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 : 8 ( 6 usr; 7 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 32 ( 0 sgn 32 !; 0 ?; 24 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : add(X0,X1) = add(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/ROB001-0.ax',commutativity_of_add) ).
fof(f2,axiom,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/ROB001-0.ax',associativity_of_add) ).
fof(f3,axiom,
! [X0,X1] : negate(add(negate(add(X0,X1)),negate(add(X0,negate(X1))))) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/ROB001-0.ax',robbins_axiom) ).
fof(f4,axiom,
! [X0] : multiply(one,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/ROB001-1.ax',one_times_x) ).
fof(f10,axiom,
negate(add(negate(e),negate(add(d,negate(e))))) = d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condition) ).
fof(f11,plain,
d = negate(add(negate(e),negate(add(d,negate(e))))),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))) != negate(e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_base_step) ).
fof(f13,plain,
negate(e) != negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))),
inference(reorient_equations,[],[f12]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] : add(X0,X1) = add(X1,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
inference(cnf_transformation,[],[f2]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] : negate(add(negate(add(X0,X1)),negate(add(X0,negate(X1))))) = X0,
inference(cnf_transformation,[],[f3]) ).
tcf(c_63,plain,
! [X0: $i] : multiply(one,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_69,plain,
negate(add(negate(e),negate(add(d,negate(e))))) = d,
inference(cnf_transformation,[],[f11]) ).
tcf(c_70,negated_conjecture,
negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))) != negate(e),
inference(cnf_transformation,[],[f13]) ).
tcf(c_115,plain,
negate(add(e,add(d,negate(add(d,negate(e)))))) != negate(e),
inference(demodulation,[status(thm)],[c_70,c_63]) ).
tcf(c_131,definition,
iPr_def_10 = negate(e),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_132,definition,
iPr_def_11 = add(d,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_133,definition,
iPr_def_12 = negate(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_134,definition,
iPr_def_13 = add(d,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_135,definition,
iPr_def_14 = add(e,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_136,definition,
iPr_def_15 = negate(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_137,plain,
iPr_def_15 != iPr_def_10,
inference(demodulation,[status(thm)],[c_115,c_131,c_132,c_133,c_134,c_135,c_136]) ).
tcf(c_295,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,X2)) = add(X1,add(X0,X2)),
inference(superposition,[status(thm)],[c_61,c_60]) ).
tcf(c_300,plain,
add(iPr_def_10,d) = iPr_def_11,
inference(theory_normalisation,[status(thm)],[c_132,c_61,c_60]) ).
tcf(c_301,plain,
add(iPr_def_12,d) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_134,c_61,c_60]) ).
tcf(c_302,plain,
add(iPr_def_13,e) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_135,c_61,c_60]) ).
tcf(c_309,plain,
negate(add(iPr_def_10,negate(add(d,iPr_def_10)))) = d,
inference(light_normalisation,[status(thm)],[c_69,c_131]) ).
tcf(c_310,plain,
negate(add(iPr_def_10,iPr_def_12)) = d,
inference(demodulation,[status(thm)],[c_309,c_60,c_133,c_300]) ).
tcf(c_370,plain,
! [X0: $i] : add(iPr_def_10,add(X0,d)) = add(X0,iPr_def_11),
inference(superposition,[status(thm)],[c_300,c_295]) ).
tcf(c_371,plain,
! [X0: $i] : add(iPr_def_12,add(X0,d)) = add(X0,iPr_def_13),
inference(superposition,[status(thm)],[c_301,c_295]) ).
tcf(c_411,plain,
! [X0: $i] : add(iPr_def_10,add(d,X0)) = add(X0,iPr_def_11),
inference(superposition,[status(thm)],[c_60,c_370]) ).
tcf(c_550,plain,
! [X0: $i,X1: $i] : negate(add(negate(add(X0,X1)),negate(add(X1,negate(X0))))) = X1,
inference(superposition,[status(thm)],[c_60,c_62]) ).
tcf(c_557,plain,
negate(add(negate(iPr_def_14),negate(add(iPr_def_13,negate(e))))) = iPr_def_13,
inference(superposition,[status(thm)],[c_302,c_62]) ).
tcf(c_558,plain,
! [X0: $i] : negate(add(negate(add(X0,iPr_def_11)),negate(add(iPr_def_10,negate(add(d,X0)))))) = iPr_def_10,
inference(superposition,[status(thm)],[c_411,c_62]) ).
tcf(c_574,plain,
! [X0: $i] : negate(add(negate(add(X0,e)),negate(add(X0,iPr_def_10)))) = X0,
inference(superposition,[status(thm)],[c_131,c_62]) ).
tcf(c_576,plain,
! [X0: $i] : negate(add(negate(add(X0,iPr_def_11)),negate(add(X0,iPr_def_12)))) = X0,
inference(superposition,[status(thm)],[c_133,c_62]) ).
tcf(c_577,plain,
! [X0: $i] : negate(add(negate(add(X0,iPr_def_14)),negate(add(X0,iPr_def_15)))) = X0,
inference(superposition,[status(thm)],[c_136,c_62]) ).
tcf(c_582,plain,
negate(add(iPr_def_15,negate(add(iPr_def_13,iPr_def_10)))) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_557,c_131,c_136]) ).
tcf(c_583,plain,
negate(add(iPr_def_15,negate(add(iPr_def_10,iPr_def_13)))) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_582,c_61,c_60]) ).
tcf(c_585,plain,
! [X0: $i] : negate(add(negate(add(X0,iPr_def_10)),negate(add(X0,e)))) = X0,
inference(theory_normalisation,[status(thm)],[c_574,c_61,c_60]) ).
tcf(c_926,plain,
negate(add(negate(add(iPr_def_15,add(iPr_def_10,iPr_def_13))),iPr_def_13)) = iPr_def_15,
inference(superposition,[status(thm)],[c_583,c_62]) ).
tcf(c_928,plain,
negate(add(iPr_def_13,negate(add(iPr_def_10,add(iPr_def_13,iPr_def_15))))) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_926,c_61,c_60]) ).
tcf(c_1522,plain,
! [X0: $i] : negate(add(negate(add(X0,iPr_def_11)),negate(add(iPr_def_12,X0)))) = X0,
inference(superposition,[status(thm)],[c_60,c_576]) ).
tcf(c_1677,plain,
! [X0: $i] : negate(add(negate(add(X0,iPr_def_14)),negate(add(iPr_def_15,X0)))) = X0,
inference(superposition,[status(thm)],[c_60,c_577]) ).
tcf(c_1717,plain,
! [X0: $i] : negate(add(negate(add(iPr_def_10,X0)),negate(add(X0,e)))) = X0,
inference(superposition,[status(thm)],[c_60,c_585]) ).
tcf(c_2244,plain,
negate(add(d,negate(add(iPr_def_12,e)))) = iPr_def_12,
inference(superposition,[status(thm)],[c_310,c_1717]) ).
tcf(c_2252,plain,
negate(add(negate(iPr_def_11),negate(add(d,e)))) = d,
inference(superposition,[status(thm)],[c_300,c_1717]) ).
tcf(c_2272,plain,
negate(add(negate(iPr_def_11),negate(add(e,d)))) = d,
inference(theory_normalisation,[status(thm)],[c_2252,c_61,c_60]) ).
tcf(c_2273,plain,
negate(add(iPr_def_12,negate(add(e,d)))) = d,
inference(light_normalisation,[status(thm)],[c_2272,c_133]) ).
tcf(c_2357,plain,
negate(add(negate(add(d,add(iPr_def_12,e))),iPr_def_12)) = d,
inference(superposition,[status(thm)],[c_2244,c_62]) ).
tcf(c_2359,plain,
negate(add(iPr_def_12,negate(add(iPr_def_12,add(e,d))))) = d,
inference(theory_normalisation,[status(thm)],[c_2357,c_61,c_60]) ).
tcf(c_2378,plain,
negate(add(negate(add(iPr_def_12,add(e,d))),d)) = iPr_def_12,
inference(superposition,[status(thm)],[c_2273,c_62]) ).
tcf(c_2381,plain,
negate(add(d,negate(add(iPr_def_12,add(e,d))))) = iPr_def_12,
inference(theory_normalisation,[status(thm)],[c_2378,c_61,c_60]) ).
tcf(c_2403,plain,
negate(add(iPr_def_12,iPr_def_15)) = d,
inference(demodulation,[status(thm)],[c_2359,c_60,c_136,c_302,c_371]) ).
tcf(c_2409,plain,
negate(add(negate(add(iPr_def_12,iPr_def_14)),d)) = iPr_def_12,
inference(superposition,[status(thm)],[c_2403,c_577]) ).
tcf(c_2412,plain,
negate(add(d,negate(add(iPr_def_12,iPr_def_14)))) = iPr_def_12,
inference(theory_normalisation,[status(thm)],[c_2409,c_61,c_60]) ).
tcf(c_2560,plain,
negate(add(negate(add(d,add(iPr_def_12,iPr_def_14))),iPr_def_12)) = d,
inference(superposition,[status(thm)],[c_2412,c_62]) ).
tcf(c_2562,plain,
negate(add(iPr_def_12,negate(add(iPr_def_12,add(iPr_def_14,d))))) = d,
inference(theory_normalisation,[status(thm)],[c_2560,c_61,c_60]) ).
tcf(c_2600,plain,
negate(add(iPr_def_15,d)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_2381,c_60,c_136,c_302,c_371]) ).
tcf(c_2605,plain,
negate(add(negate(add(d,iPr_def_14)),iPr_def_12)) = d,
inference(superposition,[status(thm)],[c_2600,c_1677]) ).
tcf(c_2606,plain,
negate(add(iPr_def_12,negate(add(iPr_def_14,d)))) = d,
inference(theory_normalisation,[status(thm)],[c_2605,c_61,c_60]) ).
tcf(c_2621,plain,
negate(add(negate(add(iPr_def_12,add(iPr_def_14,d))),d)) = iPr_def_12,
inference(superposition,[status(thm)],[c_2606,c_62]) ).
tcf(c_2624,plain,
negate(add(d,negate(add(iPr_def_12,add(iPr_def_14,d))))) = iPr_def_12,
inference(theory_normalisation,[status(thm)],[c_2621,c_61,c_60]) ).
tcf(c_2682,plain,
negate(add(iPr_def_12,negate(add(iPr_def_13,iPr_def_14)))) = d,
inference(demodulation,[status(thm)],[c_2562,c_60,c_371]) ).
tcf(c_2688,plain,
negate(add(negate(add(negate(add(iPr_def_13,iPr_def_14)),iPr_def_11)),d)) = negate(add(iPr_def_13,iPr_def_14)),
inference(superposition,[status(thm)],[c_2682,c_1522]) ).
tcf(c_2690,plain,
negate(add(d,negate(add(iPr_def_11,negate(add(iPr_def_13,iPr_def_14)))))) = negate(add(iPr_def_13,iPr_def_14)),
inference(theory_normalisation,[status(thm)],[c_2688,c_61,c_60]) ).
tcf(c_2703,plain,
negate(add(d,negate(add(iPr_def_13,iPr_def_14)))) = iPr_def_12,
inference(demodulation,[status(thm)],[c_2624,c_60,c_371]) ).
tcf(c_14720,plain,
negate(add(negate(add(negate(add(iPr_def_13,iPr_def_14)),iPr_def_11)),negate(add(iPr_def_10,iPr_def_12)))) = iPr_def_10,
inference(superposition,[status(thm)],[c_2703,c_558]) ).
tcf(c_14750,plain,
negate(add(negate(add(iPr_def_10,iPr_def_12)),negate(add(iPr_def_11,negate(add(iPr_def_13,iPr_def_14)))))) = iPr_def_10,
inference(theory_normalisation,[status(thm)],[c_14720,c_61,c_60]) ).
tcf(c_14751,plain,
negate(add(iPr_def_13,iPr_def_14)) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_14750,c_310,c_2690]) ).
tcf(c_15269,plain,
negate(add(iPr_def_10,negate(add(iPr_def_13,iPr_def_15)))) = iPr_def_13,
inference(superposition,[status(thm)],[c_14751,c_577]) ).
tcf(c_15408,plain,
negate(add(negate(add(add(iPr_def_13,iPr_def_15),iPr_def_10)),iPr_def_13)) = iPr_def_10,
inference(superposition,[status(thm)],[c_15269,c_550]) ).
tcf(c_15409,plain,
negate(add(iPr_def_13,negate(add(iPr_def_10,add(iPr_def_13,iPr_def_15))))) = iPr_def_10,
inference(theory_normalisation,[status(thm)],[c_15408,c_61,c_60]) ).
tcf(c_15421,plain,
iPr_def_10 = iPr_def_15,
inference(demodulation,[status(thm)],[c_928,c_15409]) ).
tcf(c_15450,plain,
iPr_def_10 != iPr_def_10,
inference(demodulation,[status(thm)],[c_137,c_15421]) ).
tcf(c_15451,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_15450]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ROB014-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.07/0.35 % Computer : n018.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Thu Sep 24 08:29:03 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 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.13/0.40
% 0.13/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.40
% 0.13/0.40 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 10.31/2.27 % SZS status Started for theBenchmark.p
% 10.31/2.27 % SZS status Unsatisfiable for theBenchmark.p
% 10.31/2.27
% 10.31/2.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.31/2.27
% 10.31/2.27 % ------ iProver source info
% 10.31/2.27
% 10.31/2.27 % git: date: 2026-07-19 20:42:38 +0200
% 10.31/2.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.31/2.27 % git: non_committed_changes: false
% 10.31/2.27
% 10.31/2.27 % ------ Parsing...% successful
% 10.31/2.27
% 10.31/2.27
% 10.31/2.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 10.31/2.27
% 10.31/2.27 % ------ Preprocessing... sup_sim: 1 sf_s rm: 1 0s sf_e pe_s pe_e %
% 10.31/2.27
% 10.31/2.27 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 10.31/2.27
% 10.31/2.27 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 10.31/2.27 % ------ Proving...
% 10.31/2.27 % ------ Problem Properties
% 10.31/2.27
% 10.31/2.27 %
% 10.31/2.27 % clauses 17
% 10.31/2.27 % conjectures 0
% 10.31/2.27 % EPR 2
% 10.31/2.27 % Horn 17
% 10.31/2.27 % unary 13
% 10.31/2.27 % binary 4
% 10.31/2.27 % lits 21
% 10.31/2.27 % lits eq 16
% 10.31/2.27 % fd_pure 0
% 10.31/2.27 % fd_pseudo 0
% 10.31/2.27 % fd_cond 0
% 10.31/2.27 % fd_pseudo_cond 1
% 10.31/2.27 % AC symbols 1
% 10.31/2.27
% 10.31/2.27 % ------ Schedule dynamic 5 is on
% 10.31/2.27
% 10.31/2.27 % ------ no conjectures: strip conj schedule
% 10.31/2.27
% 10.31/2.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 10.31/2.27
% 10.31/2.27
% 10.31/2.27 % ------
% 10.31/2.27 % Current options:
% 10.31/2.27 % ------
% 10.31/2.27
% 10.31/2.27
% 10.31/2.27 %
% 10.31/2.27
% 10.31/2.27 % ------ Proving...
% 10.31/2.27 %
% 10.31/2.27
% 10.31/2.27 % SZS status Unsatisfiable for theBenchmark.p
% 10.31/2.27
% 10.31/2.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.31/2.27
% 10.31/2.27
%------------------------------------------------------------------------------