%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KLE135+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n007.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 01:52:28 PM UTC 2026
% Result : Theorem 102.21s 16.88s
% Output : CNFRefutation 102.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 15
% Syntax : Number of formulae : 90 ( 78 unt; 0 def)
% Number of atoms : 102 ( 101 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 26 ( 14 ~; 7 |; 2 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 128 ( 0 sgn 127 !; 1 ?; 68 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_associativity) ).
fof(f3,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_identity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_idempotence) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',multiplicative_left_identity) ).
fof(f8,axiom,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',right_distributivity) ).
fof(f9,axiom,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',left_distributivity) ).
fof(f13,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',domain1) ).
fof(f15,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',domain3) ).
fof(f16,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',domain4) ).
fof(f23,axiom,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+6.ax',forward_diamond) ).
fof(f27,axiom,
! [X0] : forward_diamond(X0,divergence(X0)) = divergence(X0),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+7.ax',divergence1) ).
fof(f28,axiom,
! [X0,X1,X2] :
( addition(domain(X0),addition(forward_diamond(X1,domain(X0)),domain(X2))) = addition(forward_diamond(X1,domain(X0)),domain(X2))
=> addition(domain(X0),addition(divergence(X1),forward_diamond(star(X1),domain(X2)))) = addition(divergence(X1),forward_diamond(star(X1),domain(X2))) ),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+7.ax',divergence2) ).
fof(f29,conjecture,
! [X0] :
( divergence(X0) = zero
=> forward_diamond(star(X0),antidomain(X0)) = one ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f30,negated_conjecture,
~ ! [X0] :
( divergence(X0) = zero
=> forward_diamond(star(X0),antidomain(X0)) = one ),
inference(negated_conjecture,[status(cth)],[f29]) ).
fof(f31,plain,
? [X0] :
( divergence(X0) = zero
& one != forward_diamond(star(X0),antidomain(X0)) ),
inference(ennf_transformation,[],[f30]) ).
fof(f32,plain,
! [X0,X1,X2] :
( addition(forward_diamond(X1,domain(X0)),domain(X2)) != addition(domain(X0),addition(forward_diamond(X1,domain(X0)),domain(X2)))
| addition(domain(X0),addition(divergence(X1),forward_diamond(star(X1),domain(X2)))) = addition(divergence(X1),forward_diamond(star(X1),domain(X2))) ),
inference(ennf_transformation,[],[f28]) ).
fof(f33,plain,
( zero = divergence(sK0)
& one != forward_diamond(star(sK0),antidomain(sK0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f31]) ).
fof(f34,plain,
zero = divergence(sK0),
inference(cnf_transformation,[],[f33]) ).
fof(f35,plain,
one != forward_diamond(star(sK0),antidomain(sK0)),
inference(cnf_transformation,[],[f33]) ).
fof(f37,plain,
! [X0] : zero = multiplication(antidomain(X0),X0),
inference(cnf_transformation,[],[f13]) ).
fof(f40,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f42,plain,
! [X0] : one = addition(antidomain(antidomain(X0)),antidomain(X0)),
inference(cnf_transformation,[],[f15]) ).
fof(f43,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f44,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f45,plain,
! [X0] : antidomain(antidomain(X0)) = domain(X0),
inference(cnf_transformation,[],[f16]) ).
fof(f47,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(cnf_transformation,[],[f23]) ).
fof(f48,plain,
! [X2,X0,X1] :
( addition(forward_diamond(X1,domain(X0)),domain(X2)) != addition(domain(X0),addition(forward_diamond(X1,domain(X0)),domain(X2)))
| addition(divergence(X1),forward_diamond(star(X1),domain(X2))) = addition(domain(X0),addition(divergence(X1),forward_diamond(star(X1),domain(X2)))) ),
inference(cnf_transformation,[],[f32]) ).
fof(f49,plain,
! [X0] : divergence(X0) = forward_diamond(X0,divergence(X0)),
inference(cnf_transformation,[],[f27]) ).
fof(f50,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f51,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f54,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f55,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f56,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f57,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f47,f45,f45]) ).
fof(f58,plain,
one != antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(antidomain(sK0)))))),
inference(definition_unfolding,[],[f35,f57]) ).
fof(f59,plain,
! [X2,X0,X1] :
( addition(antidomain(antidomain(multiplication(X1,antidomain(antidomain(antidomain(antidomain(X0))))))),antidomain(antidomain(X2))) != addition(antidomain(antidomain(X0)),addition(antidomain(antidomain(multiplication(X1,antidomain(antidomain(antidomain(antidomain(X0))))))),antidomain(antidomain(X2))))
| addition(divergence(X1),antidomain(antidomain(multiplication(star(X1),antidomain(antidomain(antidomain(antidomain(X2)))))))) = addition(antidomain(antidomain(X0)),addition(divergence(X1),antidomain(antidomain(multiplication(star(X1),antidomain(antidomain(antidomain(antidomain(X2))))))))) ),
inference(definition_unfolding,[],[f48,f57,f45,f45,f57,f45,f57,f45,f45,f45,f57,f45,f45]) ).
fof(f60,plain,
! [X0] : divergence(X0) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(divergence(X0)))))),
inference(definition_unfolding,[],[f49,f57]) ).
tcf(c_49,negated_conjecture,
antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(antidomain(sK0)))))) != one,
inference(cnf_transformation,[],[f58]) ).
tcf(c_50,negated_conjecture,
divergence(sK0) = zero,
inference(cnf_transformation,[],[f34]) ).
tcf(c_52,plain,
! [X0: $i] : multiplication(antidomain(X0),X0) = zero,
inference(cnf_transformation,[],[f37]) ).
tcf(c_55,plain,
! [X0: $i] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f40]) ).
tcf(c_57,plain,
! [X0: $i] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
inference(cnf_transformation,[],[f42]) ).
tcf(c_58,plain,
! [X0: $i] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f43]) ).
tcf(c_59,plain,
! [X0: $i] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f44]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( addition(antidomain(antidomain(X0)),addition(divergence(X1),antidomain(antidomain(multiplication(star(X1),antidomain(antidomain(antidomain(antidomain(X2))))))))) = addition(divergence(X1),antidomain(antidomain(multiplication(star(X1),antidomain(antidomain(antidomain(antidomain(X2)))))))) )
| ( addition(antidomain(antidomain(X0)),addition(antidomain(antidomain(multiplication(X1,antidomain(antidomain(antidomain(antidomain(X0))))))),antidomain(antidomain(X2)))) != addition(antidomain(antidomain(multiplication(X1,antidomain(antidomain(antidomain(antidomain(X0))))))),antidomain(antidomain(X2))) ) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_62,plain,
! [X0: $i] : antidomain(antidomain(multiplication(X0,antidomain(antidomain(divergence(X0)))))) = divergence(X0),
inference(cnf_transformation,[],[f60]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X2,X1)) = multiplication(addition(X0,X2),X1),
inference(cnf_transformation,[],[f50]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X0,X2)) = multiplication(X0,addition(X1,X2)),
inference(cnf_transformation,[],[f51]) ).
tcf(c_67,plain,
! [X0: $i] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f54]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i] : addition(addition(X0,X1),X2) = addition(X0,addition(X1,X2)),
inference(cnf_transformation,[],[f55]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f56]) ).
tcf(c_88,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = one,
inference(theory_normalisation,[status(thm)],[c_57,c_68,c_69]) ).
tcf(c_150608,plain,
! [X0: $i,X1: $i,X2: $i] : addition(X0,addition(X1,X2)) = addition(X1,addition(X0,X2)),
inference(superposition,[status(thm)],[c_68,c_69]) ).
tcf(c_150612,plain,
antidomain(one) = zero,
inference(superposition,[status(thm)],[c_59,c_52]) ).
tcf(c_150614,plain,
! [X0: $i] : addition(zero,X0) = X0,
inference(superposition,[status(thm)],[c_55,c_69]) ).
tcf(c_150620,plain,
addition(zero,antidomain(zero)) = one,
inference(superposition,[status(thm)],[c_150612,c_88]) ).
tcf(c_150630,plain,
antidomain(zero) = one,
inference(demodulation,[status(thm)],[c_150620,c_150614]) ).
tcf(c_150637,plain,
! [X0: $i] : addition(divergence(X0),antidomain(divergence(X0))) = one,
inference(superposition,[status(thm)],[c_62,c_88]) ).
tcf(c_150672,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_67,c_68]) ).
tcf(c_150683,plain,
! [X0: $i,X1: $i] : multiplication(addition(antidomain(X0),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(superposition,[status(thm)],[c_52,c_63]) ).
tcf(c_150736,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X0,X1)) = addition(zero,multiplication(antidomain(X0),X1)),
inference(superposition,[status(thm)],[c_52,c_64]) ).
tcf(c_150816,plain,
! [X0: $i] : addition(antidomain(X0),one) = one,
inference(superposition,[status(thm)],[c_88,c_150672]) ).
tcf(c_150817,plain,
! [X0: $i] : addition(divergence(X0),one) = one,
inference(superposition,[status(thm)],[c_150637,c_150672]) ).
tcf(c_150820,plain,
! [X0: $i] : addition(one,divergence(X0)) = one,
inference(theory_normalisation,[status(thm)],[c_150817,c_68,c_69]) ).
tcf(c_150821,plain,
! [X0: $i] : addition(one,antidomain(X0)) = one,
inference(theory_normalisation,[status(thm)],[c_150816,c_68,c_69]) ).
tcf(c_150838,plain,
! [X0: $i,X1: $i] : addition(one,addition(antidomain(X0),X1)) = addition(one,X1),
inference(superposition,[status(thm)],[c_150821,c_68]) ).
tcf(c_151002,plain,
! [X0: $i,X1: $i] :
( ( addition(antidomain(antidomain(one)),addition(divergence(X0),antidomain(antidomain(multiplication(star(X0),antidomain(antidomain(antidomain(antidomain(X1))))))))) = addition(divergence(X0),antidomain(antidomain(multiplication(star(X0),antidomain(antidomain(antidomain(antidomain(X1)))))))) )
| ( addition(antidomain(zero),addition(antidomain(antidomain(multiplication(X0,antidomain(antidomain(antidomain(zero)))))),antidomain(antidomain(X1)))) != addition(antidomain(antidomain(multiplication(X0,antidomain(antidomain(antidomain(zero)))))),antidomain(antidomain(X1))) ) ),
inference(superposition,[status(thm)],[c_150612,c_61]) ).
tcf(c_151022,plain,
! [X0: $i,X1: $i] :
( ( addition(one,addition(divergence(X0),antidomain(antidomain(multiplication(star(X0),antidomain(antidomain(antidomain(antidomain(X1))))))))) = addition(divergence(X0),antidomain(antidomain(multiplication(star(X0),antidomain(antidomain(antidomain(antidomain(X1)))))))) )
| ( addition(one,addition(antidomain(antidomain(X0)),antidomain(antidomain(X1)))) != addition(antidomain(antidomain(X0)),antidomain(antidomain(X1))) ) ),
inference(light_normalisation,[status(thm)],[c_151002,c_59,c_150612,c_150630]) ).
tcf(c_151594,plain,
! [X0: $i,X1: $i] : addition(antidomain(X0),addition(X1,antidomain(antidomain(X0)))) = addition(X1,one),
inference(superposition,[status(thm)],[c_88,c_150608]) ).
tcf(c_151599,plain,
! [X0: $i,X1: $i] : addition(one,addition(X0,divergence(X1))) = addition(X0,one),
inference(superposition,[status(thm)],[c_150820,c_150608]) ).
tcf(c_151679,plain,
! [X0: $i,X1: $i] : addition(one,addition(divergence(X0),X1)) = addition(X1,one),
inference(superposition,[status(thm)],[c_69,c_151599]) ).
tcf(c_151684,plain,
! [X0: $i] : addition(one,addition(X0,one)) = addition(X0,one),
inference(superposition,[status(thm)],[c_151599,c_150672]) ).
tcf(c_156189,plain,
! [X0: $i,X1: $i] : multiplication(addition(antidomain(X0),X1),X0) = multiplication(X1,X0),
inference(demodulation,[status(thm)],[c_150683,c_150614]) ).
tcf(c_156197,plain,
! [X0: $i] : multiplication(antidomain(antidomain(X0)),X0) = multiplication(one,X0),
inference(superposition,[status(thm)],[c_88,c_156189]) ).
tcf(c_156232,plain,
! [X0: $i] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(light_normalisation,[status(thm)],[c_156197,c_58]) ).
tcf(c_165836,plain,
! [X0: $i,X1: $i] : addition(antidomain(X0),addition(antidomain(antidomain(X0)),X1)) = addition(X1,one),
inference(superposition,[status(thm)],[c_69,c_151594]) ).
tcf(c_170416,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X0,X1)) = multiplication(antidomain(X0),X1),
inference(demodulation,[status(thm)],[c_150736,c_150614]) ).
tcf(c_170429,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X1,X0)) = multiplication(antidomain(X0),X1),
inference(superposition,[status(thm)],[c_69,c_170416]) ).
tcf(c_170753,plain,
! [X0: $i] : multiplication(antidomain(antidomain(antidomain(X0))),antidomain(X0)) = multiplication(antidomain(antidomain(antidomain(X0))),one),
inference(superposition,[status(thm)],[c_88,c_170429]) ).
tcf(c_172436,plain,
! [X0: $i,X1: $i] : addition(one,addition(antidomain(antidomain(X0)),X1)) = addition(one,addition(X1,one)),
inference(superposition,[status(thm)],[c_165836,c_150838]) ).
tcf(c_225638,plain,
! [X0: $i] : antidomain(antidomain(antidomain(X0))) = antidomain(X0),
inference(demodulation,[status(thm)],[c_170753,c_59,c_156232]) ).
tcf(c_225639,plain,
antidomain(antidomain(multiplication(star(sK0),antidomain(sK0)))) != one,
inference(demodulation,[status(thm)],[c_49,c_225638]) ).
tcf(c_227213,plain,
! [X0: $i,X1: $i] :
( ( addition(divergence(X0),antidomain(antidomain(multiplication(star(X0),antidomain(antidomain(X1)))))) = one )
| ( addition(antidomain(antidomain(X0)),antidomain(antidomain(X1))) != one ) ),
inference(demodulation,[status(thm)],[c_151022,c_67,c_69,c_150821,c_151679,c_151684,c_172436,c_225638]) ).
tcf(c_227219,plain,
! [X0: $i] : addition(divergence(X0),antidomain(antidomain(multiplication(star(X0),antidomain(antidomain(antidomain(X0))))))) = one,
inference(superposition,[status(thm)],[c_88,c_227213]) ).
tcf(c_227274,plain,
! [X0: $i] : addition(divergence(X0),antidomain(antidomain(multiplication(star(X0),antidomain(X0))))) = one,
inference(light_normalisation,[status(thm)],[c_227219,c_225638]) ).
tcf(c_228461,plain,
addition(zero,antidomain(antidomain(multiplication(star(sK0),antidomain(sK0))))) = one,
inference(superposition,[status(thm)],[c_50,c_227274]) ).
tcf(c_228744,plain,
antidomain(antidomain(multiplication(star(sK0),antidomain(sK0)))) = one,
inference(demodulation,[status(thm)],[c_228461,c_150614]) ).
tcf(c_228745,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_228744,c_225639]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE135+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n007.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 19:00:22 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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.11/0.43
% 0.11/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.43
% 0.11/0.43 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 102.21/16.88 % SZS status Started for theBenchmark.p
% 102.21/16.88 ERROR - "ProverProcess:heur/330959:296.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( addition(one,divergence(one)) = divergence(one) )")
% 102.21/16.88 Fatal error: exception Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( addition(one,divergence(one)) = divergence(one) )")
% 102.21/16.88 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_af_restrict_to_split_sk false --abstr_ref_prep false --abstr_ref_sig_restrict funpre --abstr_ref_under "[]" --abstr_ref_until_sat false --add_important_lit false --bc_imp_inh "[conj_cone]" --brand_transform false --clause_weak_htbl true --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --gc_record_bc_elim false --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_sos_phase true --inst_sos_sth_lit_sel "[+prop;+non_prol_conj_symb;-eq;+ground;-num_var]" --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --large_theory_mode true --lt_threshold 2000 --min_unsat_core false --non_eq_to_eq false --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sem_filter_out false --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessed_out false --preprocessed_stats false --preprocessing_flag true --prolific_symb_bound 256 --prop_impl_unit "[]" --prop_impl_unit_size 0 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_orphan_elimination true --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300. --res_to_prop_solver active --reset_solvers false --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --soft_assumptions false --soft_lemma_size 3 --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[BwDemod;BwUnitSubsAndRes]" --sup_full_fw "[FwDemodLightNormLoopTriv;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[BwUnitSubsAndRes]" --sup_immed_bw_main "[BwUnitSubsAndRes]" --sup_immed_fw_immed "[ACNormalisation;FwDemodLightNormLoopTriv;FwUnitSubsAndRes]" --sup_immed_fw_main "[FwUnitSubsAndRes]" --sup_immed_triv "[]" --sup_indices_passive "[LightNormIndex;UnitSubsumptionIndex]" --sup_input_bw "[BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]" --sup_input_fw "[ACNormalisation;FwDemodLightNormLoopTriv;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --out_options none --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 98.67" --time_out_real 296.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_odaq303h/rqco3l5w 2>> /export/starexec/sandbox/tmp/iprover_out_odaq303h/rqco3l5w_error
% 102.21/16.88 % SZS status Theorem for theBenchmark.p
% 102.21/16.88
% 102.21/16.88 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 102.21/16.88
% 102.21/16.88 % ------ iProver source info
% 102.21/16.88
% 102.21/16.88 % git: date: 2026-07-19 20:42:38 +0200
% 102.21/16.88 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 102.21/16.88 % git: non_committed_changes: false
% 102.21/16.88
% 102.21/16.88 % ------ Parsing...
% 102.21/16.88 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 102.21/16.88
% 102.21/16.88 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 102.21/16.88
% 102.21/16.88 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 102.21/16.88
% 102.21/16.88 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 102.21/16.88 % ------ Proving...
% 102.21/16.88 % ------ Problem Properties
% 102.21/16.88
% 102.21/16.88 %
% 102.21/16.88 % clauses 21
% 102.21/16.88 % conjectures 2
% 102.21/16.88 % EPR 0
% 102.21/16.88 % Horn 21
% 102.21/16.88 % unary 20
% 102.21/16.88 % binary 1
% 102.21/16.88 % lits 22
% 102.21/16.88 % lits eq 22
% 102.21/16.88 % fd_pure 0
% 102.21/16.88 % fd_pseudo 0
% 102.21/16.88 % fd_cond 0
% 102.21/16.88 % fd_pseudo_cond 0
% 102.21/16.88 % AC symbols 1
% 102.21/16.88
% 102.21/16.88 % ------ Schedule dynamic 5 is on
% 102.21/16.88
% 102.21/16.88 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 102.21/16.88
% 102.21/16.88
% 102.21/16.88 % ------
% 102.21/16.88 % Current options:
% 102.21/16.88 % ------
% 102.21/16.88
% 102.21/16.88
% 102.21/16.88 %
% 102.21/16.88
% 102.21/16.88 % ------ Proving...
% 102.21/16.88 % Proof_search_loop: time out after: 3495 full_loop iterations
% 102.21/16.88
% 102.21/16.88 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 102.21/16.88
% 102.21/16.88
% 102.21/16.88 % ------
% 102.21/16.88 % Current options:
% 102.21/16.88 % ------
% 102.21/16.88
% 102.21/16.88
% 102.21/16.88 %
% 102.21/16.88
% 102.21/16.88 % ------ Proving...
% 102.21/16.88 %
% 102.21/16.88
% 102.21/16.88 % SZS status Theorem for theBenchmark.p
% 102.21/16.88
% 102.21/16.88 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 102.21/16.88
% 102.21/16.88
%------------------------------------------------------------------------------