%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT005-4 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n010.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:58:04 PM UTC 2026
% Result : Unsatisfiable 74.92s 19.05s
% Output : CNFRefutation 74.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 15
% Syntax : Number of formulae : 100 ( 90 unt; 0 def)
% Number of atoms : 118 ( 117 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 40 ( 22 ~; 18 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 6 ( 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 : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 122 ( 0 sgn 122 !; 0 ?; 104 :)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-0.ax',associativity_of_join) ).
fof(f11,axiom,
! [X0] : join(X0,n0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-1.ax',x_join_0) ).
fof(f15,axiom,
! [X2,X0,X1] :
( meet(X1,join(X0,X2)) = join(X0,meet(X2,X1))
| meet(X0,X1) != X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/LAT001-1.ax',modular) ).
fof(f18,negated_conjecture,
meet(r2,meet(a,b)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',r2_complement_meet_a_b_2) ).
fof(f19,plain,
n0 = meet(r2,meet(a,b)),
inference(reorient_equations,[],[f18]) ).
fof(f22,negated_conjecture,
meet(r1,join(a,b)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',r1_complement_join_a_b_2) ).
fof(f23,plain,
n0 = meet(r1,join(a,b)),
inference(reorient_equations,[],[f22]) ).
fof(f24,negated_conjecture,
join(r1,meet(a,r2)) = b2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',define_b2) ).
fof(f25,negated_conjecture,
join(r1,meet(b,r2)) = a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',define_a2) ).
fof(f26,negated_conjecture,
meet(a2,b2) != r1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_SAMs_lemma) ).
fof(f27,plain,
r1 != meet(a2,b2),
inference(reorient_equations,[],[f26]) ).
tcf(c_70,negated_conjecture,
meet(r2,meet(a,b)) = n0,
inference(cnf_transformation,[],[f19]) ).
tcf(c_72,negated_conjecture,
meet(r1,join(a,b)) = n0,
inference(cnf_transformation,[],[f23]) ).
tcf(c_73,negated_conjecture,
join(r1,meet(a,r2)) = b2,
inference(cnf_transformation,[],[f24]) ).
tcf(c_74,negated_conjecture,
join(r1,meet(b,r2)) = a2,
inference(cnf_transformation,[],[f25]) ).
tcf(c_75,negated_conjecture,
meet(a2,b2) != r1,
inference(cnf_transformation,[],[f27]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i,X2: $i] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i] : meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[],[f5]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( meet(X1,join(X0,X2)) = join(X0,meet(X2,X1)) )
| ( meet(X0,X1) != X0 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] : join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] : meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[],[f3]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[],[f8]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f6]) ).
tcf(c_87,plain,
! [X0: $i] : join(X0,n0) = X0,
inference(cnf_transformation,[],[f11]) ).
tcf(c_102,negated_conjecture,
meet(a,meet(b,r2)) = n0,
inference(theory_normalisation,[status(thm)],[c_70,c_82,c_83,c_76,c_77]) ).
tcf(c_104,negated_conjecture,
meet(b2,a2) != r1,
inference(theory_normalisation,[status(thm)],[c_75,c_82,c_83,c_76,c_77]) ).
tcf(c_153,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_154,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_398,plain,
! [X0: $i] :
( ( meet(b2,a2) = r1 )
| ( r1 != X0 )
| ( meet(b2,a2) != X0 ) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_430,plain,
! [X0: $i,X1: $i] :
( ( r1 = X0 )
| ( r1 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_431,plain,
! [X0: $i] :
( ( r1 = X0 )
| ( r1 != r1 )
| ( X0 != r1 ) ),
inference(instantiation,[status(thm)],[c_430]) ).
tcf(c_432,plain,
r1 = r1,
inference(instantiation,[status(thm)],[c_153]) ).
tcf(c_493,plain,
( ( r1 = join(r1,n0) )
| ( r1 != r1 )
| ( join(r1,n0) != r1 ) ),
inference(instantiation,[status(thm)],[c_431]) ).
tcf(c_494,plain,
join(r1,n0) = r1,
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_634,plain,
! [X0: $i] :
( ( r1 = X0 )
| ( r1 != join(r1,n0) )
| ( X0 != join(r1,n0) ) ),
inference(instantiation,[status(thm)],[c_430]) ).
tcf(c_1101,plain,
( ( r1 = join(n0,r1) )
| ( r1 != join(r1,n0) )
| ( join(n0,r1) != join(r1,n0) ) ),
inference(instantiation,[status(thm)],[c_634]) ).
tcf(c_1102,plain,
join(n0,r1) = join(r1,n0),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_4834,plain,
( ( meet(b2,a2) = r1 )
| ( r1 != join(n0,r1) )
| ( meet(b2,a2) != join(n0,r1) ) ),
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_171405,plain,
! [X0: $i,X1: $i,X2: $i] : meet(X0,meet(X1,X2)) = meet(X1,meet(X0,X2)),
inference(superposition,[status(thm)],[c_76,c_77]) ).
tcf(c_171447,plain,
! [X0: $i,X1: $i] : join(X0,meet(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_77,c_80]) ).
tcf(c_171477,plain,
meet(r1,b2) = r1,
inference(superposition,[status(thm)],[c_73,c_81]) ).
tcf(c_171499,plain,
! [X0: $i] : join(n0,X0) = X0,
inference(superposition,[status(thm)],[c_83,c_87]) ).
tcf(c_171501,plain,
! [X0: $i,X1: $i] : meet(X0,join(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_83,c_81]) ).
tcf(c_171523,plain,
! [X0: $i,X1: $i,X2: $i] : join(meet(X0,X1),meet(X0,meet(X1,X2))) = meet(X0,X1),
inference(superposition,[status(thm)],[c_76,c_80]) ).
tcf(c_171525,plain,
! [X0: $i,X1: $i,X2: $i] : meet(X0,meet(X1,join(meet(X0,X1),X2))) = meet(X0,X1),
inference(superposition,[status(thm)],[c_76,c_81]) ).
tcf(c_171535,plain,
! [X0: $i] : join(r1,join(meet(a,r2),X0)) = join(b2,X0),
inference(superposition,[status(thm)],[c_73,c_82]) ).
tcf(c_171536,plain,
! [X0: $i] : join(r1,join(meet(b,r2),X0)) = join(a2,X0),
inference(superposition,[status(thm)],[c_74,c_82]) ).
tcf(c_171570,plain,
! [X0: $i] : join(r1,join(X0,meet(a,r2))) = join(b2,X0),
inference(superposition,[status(thm)],[c_83,c_171535]) ).
tcf(c_171606,plain,
! [X0: $i] : join(a2,meet(meet(b,r2),X0)) = join(r1,meet(b,r2)),
inference(superposition,[status(thm)],[c_80,c_171536]) ).
tcf(c_171614,plain,
! [X0: $i] : join(a2,meet(b,meet(r2,X0))) = join(r1,meet(b,r2)),
inference(theory_normalisation,[status(thm)],[c_171606,c_76,c_77,c_82,c_83]) ).
tcf(c_171615,plain,
! [X0: $i] : join(a2,meet(b,meet(r2,X0))) = a2,
inference(light_normalisation,[status(thm)],[c_171614,c_74]) ).
tcf(c_171676,plain,
! [X0: $i,X1: $i,X2: $i] : meet(join(X0,X1),join(X0,X2)) = join(X0,meet(X2,join(X0,X1))),
inference(superposition,[status(thm)],[c_81,c_79]) ).
tcf(c_171682,plain,
! [X0: $i] : meet(b2,join(r1,X0)) = join(r1,meet(X0,b2)),
inference(superposition,[status(thm)],[c_171477,c_79]) ).
tcf(c_171717,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,meet(X1,meet(X2,X0))) = X0,
inference(superposition,[status(thm)],[c_76,c_171447]) ).
tcf(c_171727,plain,
! [X0: $i] : join(a2,meet(X0,meet(b,r2))) = join(r1,meet(b,r2)),
inference(superposition,[status(thm)],[c_171447,c_171536]) ).
tcf(c_171735,plain,
! [X0: $i] : join(a2,meet(X0,meet(b,r2))) = a2,
inference(light_normalisation,[status(thm)],[c_171727,c_74]) ).
tcf(c_171767,plain,
! [X0: $i,X1: $i,X2: $i] : meet(join(X0,X1),join(X1,X2)) = join(X1,meet(X2,join(X0,X1))),
inference(superposition,[status(thm)],[c_171501,c_79]) ).
tcf(c_171768,plain,
! [X0: $i,X1: $i,X2: $i] : meet(X0,meet(join(X1,X0),X2)) = meet(X0,X2),
inference(superposition,[status(thm)],[c_171501,c_76]) ).
tcf(c_171823,plain,
! [X0: $i,X1: $i] : join(a2,join(meet(X0,meet(b,r2)),X1)) = join(a2,X1),
inference(superposition,[status(thm)],[c_171735,c_82]) ).
tcf(c_172049,plain,
join(r1,a) = join(b2,a),
inference(superposition,[status(thm)],[c_80,c_171570]) ).
tcf(c_172063,plain,
join(a,r1) = join(a,b2),
inference(theory_normalisation,[status(thm)],[c_172049,c_76,c_77,c_82,c_83]) ).
tcf(c_172079,plain,
meet(b2,join(a,r1)) = b2,
inference(superposition,[status(thm)],[c_172063,c_171501]) ).
tcf(c_172091,plain,
! [X0: $i] : meet(b2,meet(join(a,r1),X0)) = meet(b2,X0),
inference(superposition,[status(thm)],[c_172079,c_76]) ).
tcf(c_172194,plain,
! [X0: $i,X1: $i] : meet(b2,join(r1,meet(X0,X1))) = join(r1,meet(X0,meet(X1,b2))),
inference(superposition,[status(thm)],[c_76,c_171682]) ).
tcf(c_172543,plain,
! [X0: $i,X1: $i] : meet(join(meet(X0,meet(b,r2)),X1),join(a2,X1)) = join(meet(X0,meet(b,r2)),X1),
inference(superposition,[status(thm)],[c_171823,c_171501]) ).
tcf(c_172555,plain,
! [X0: $i,X1: $i] : meet(join(a2,X0),join(meet(X1,meet(b,r2)),X0)) = join(meet(X1,meet(b,r2)),X0),
inference(theory_normalisation,[status(thm)],[c_172543,c_76,c_77,c_82,c_83]) ).
tcf(c_173536,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,meet(X1,meet(X0,X2))) = X0,
inference(superposition,[status(thm)],[c_77,c_171717]) ).
tcf(c_190335,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(meet(X0,X1),X2),meet(X0,X1)) = join(meet(X0,X1),X2),
inference(superposition,[status(thm)],[c_171525,c_171717]) ).
tcf(c_190407,plain,
! [X0: $i,X1: $i,X2: $i] : join(meet(X0,X1),join(X2,meet(X0,X1))) = join(meet(X0,X1),X2),
inference(theory_normalisation,[status(thm)],[c_190335,c_76,c_77,c_82,c_83]) ).
tcf(c_195530,plain,
! [X0: $i] : meet(b2,meet(X0,join(a,r1))) = meet(b2,X0),
inference(superposition,[status(thm)],[c_77,c_172091]) ).
tcf(c_197477,plain,
meet(join(a,b),join(a,r1)) = join(a,n0),
inference(superposition,[status(thm)],[c_72,c_171676]) ).
tcf(c_198755,plain,
meet(join(a,b),join(a,r1)) = a,
inference(demodulation,[status(thm)],[c_197477,c_87]) ).
tcf(c_198774,plain,
meet(b,join(a,r1)) = meet(b,a),
inference(superposition,[status(thm)],[c_198755,c_171768]) ).
tcf(c_198779,plain,
meet(b,join(a,r1)) = meet(a,b),
inference(theory_normalisation,[status(thm)],[c_198774,c_76,c_77,c_82,c_83]) ).
tcf(c_204785,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : meet(meet(X0,X1),join(meet(X0,meet(X1,X2)),X3)) = join(meet(X0,meet(X1,X2)),meet(X3,meet(X0,X1))),
inference(superposition,[status(thm)],[c_171523,c_171767]) ).
tcf(c_205208,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : meet(X0,meet(X1,join(meet(X0,meet(X1,X2)),X3))) = join(meet(X0,meet(X1,X2)),meet(X3,meet(X0,X1))),
inference(theory_normalisation,[status(thm)],[c_204785,c_76,c_77,c_82,c_83]) ).
tcf(c_233998,plain,
meet(b2,meet(a,b)) = meet(b2,b),
inference(superposition,[status(thm)],[c_198779,c_195530]) ).
tcf(c_234070,plain,
meet(a,meet(b,b2)) = meet(b,b2),
inference(theory_normalisation,[status(thm)],[c_233998,c_76,c_77,c_82,c_83]) ).
tcf(c_235691,plain,
! [X0: $i] : join(a,meet(X0,meet(b,b2))) = a,
inference(superposition,[status(thm)],[c_234070,c_173536]) ).
tcf(c_237668,plain,
! [X0: $i] : join(a,meet(b,meet(X0,b2))) = a,
inference(superposition,[status(thm)],[c_171405,c_235691]) ).
tcf(c_288729,plain,
! [X0: $i,X1: $i] : meet(a2,join(meet(X0,meet(b,r2)),meet(b,meet(r2,X1)))) = join(meet(X0,meet(b,r2)),meet(b,meet(r2,X1))),
inference(superposition,[status(thm)],[c_171615,c_172555]) ).
tcf(c_293062,plain,
! [X0: $i,X1: $i] : meet(join(meet(X0,meet(b,r2)),meet(b,meet(r2,X1))),join(meet(b,meet(r2,X1)),a2)) = join(meet(b,meet(r2,X1)),join(meet(X0,meet(b,r2)),meet(b,meet(r2,X1)))),
inference(superposition,[status(thm)],[c_288729,c_171767]) ).
tcf(c_293102,plain,
! [X0: $i,X1: $i] : meet(join(a2,meet(b,meet(r2,X0))),join(meet(X1,meet(b,r2)),meet(b,meet(r2,X0)))) = join(meet(b,meet(r2,X0)),join(meet(X1,meet(b,r2)),meet(b,meet(r2,X0)))),
inference(theory_normalisation,[status(thm)],[c_293062,c_76,c_77,c_82,c_83]) ).
tcf(c_293103,plain,
! [X0: $i,X1: $i] : join(meet(b,meet(r2,X0)),join(meet(X1,meet(b,r2)),meet(b,meet(r2,X0)))) = meet(a2,join(meet(X1,meet(b,r2)),meet(b,meet(r2,X0)))),
inference(light_normalisation,[status(thm)],[c_293102,c_171615]) ).
tcf(c_293153,plain,
! [X0: $i,X1: $i] : meet(b,meet(r2,join(meet(b,meet(r2,X0)),X1))) = join(meet(X1,meet(b,r2)),meet(b,meet(r2,X0))),
inference(demodulation,[status(thm)],[c_293103,c_190407,c_205208,c_288729]) ).
tcf(c_293167,plain,
! [X0: $i] : meet(b,meet(r2,join(meet(b,meet(r2,X0)),a))) = join(n0,meet(b,meet(r2,X0))),
inference(superposition,[status(thm)],[c_102,c_293153]) ).
tcf(c_293279,plain,
! [X0: $i] : meet(b,meet(r2,join(a,meet(b,meet(r2,X0))))) = join(n0,meet(b,meet(r2,X0))),
inference(theory_normalisation,[status(thm)],[c_293167,c_76,c_77,c_82,c_83]) ).
tcf(c_294013,plain,
! [X0: $i] : meet(b,meet(r2,join(a,meet(b,meet(r2,X0))))) = meet(b,meet(r2,X0)),
inference(demodulation,[status(thm)],[c_293279,c_171499]) ).
tcf(c_294016,plain,
meet(b,meet(r2,a)) = meet(b,meet(r2,b2)),
inference(superposition,[status(thm)],[c_237668,c_294013]) ).
tcf(c_294111,plain,
meet(a,meet(b,r2)) = meet(b,meet(r2,b2)),
inference(theory_normalisation,[status(thm)],[c_294016,c_76,c_77,c_82,c_83]) ).
tcf(c_294112,plain,
meet(b,meet(r2,b2)) = n0,
inference(light_normalisation,[status(thm)],[c_294111,c_102]) ).
tcf(c_294220,plain,
meet(b2,join(r1,meet(b,r2))) = join(r1,n0),
inference(superposition,[status(thm)],[c_294112,c_172194]) ).
tcf(c_294234,plain,
meet(b2,join(r1,meet(b,r2))) = join(n0,r1),
inference(theory_normalisation,[status(thm)],[c_294220,c_76,c_77,c_82,c_83]) ).
tcf(c_294235,plain,
meet(b2,a2) = join(n0,r1),
inference(light_normalisation,[status(thm)],[c_294234,c_74]) ).
tcf(c_294264,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_294235,c_4834,c_1102,c_1101,c_494,c_493,c_432,c_104]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT005-4 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n010.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 19:59:42 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.39 Running first-order theorem proving
% 0.12/0.39 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.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.41 % Proving...
% 74.92/19.05 % SZS status Started for theBenchmark.p
% 74.92/19.05 % SZS status Unsatisfiable for theBenchmark.p
% 74.92/19.05
% 74.92/19.05 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 74.92/19.05
% 74.92/19.05 % ------ iProver source info
% 74.92/19.05
% 74.92/19.05 % git: date: 2026-07-19 20:42:38 +0200
% 74.92/19.05 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 74.92/19.05 % git: non_committed_changes: false
% 74.92/19.05
% 74.92/19.05 % ------ Parsing...% successful
% 74.92/19.05
% 74.92/19.05
% 74.92/19.05 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 74.92/19.05
% 74.92/19.05 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 74.92/19.05
% 74.92/19.05 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 74.92/19.05
% 74.92/19.05 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 74.92/19.05 % ------ Proving...
% 74.92/19.05 % ------ Problem Properties
% 74.92/19.05
% 74.92/19.05 %
% 74.92/19.05 % clauses 20
% 74.92/19.05 % conjectures 7
% 74.92/19.05 % EPR 0
% 74.92/19.05 % Horn 20
% 74.92/19.05 % unary 19
% 74.92/19.05 % binary 1
% 74.92/19.05 % lits 21
% 74.92/19.05 % lits eq 21
% 74.92/19.06 % fd_pure 0
% 74.92/19.06 % fd_pseudo 0
% 74.92/19.06 % fd_cond 0
% 74.92/19.06 % fd_pseudo_cond 0
% 74.92/19.06 % AC symbols 2
% 74.92/19.06
% 74.92/19.06 % ------ Schedule dynamic 5 is on
% 74.92/19.06
% 74.92/19.06 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 74.92/19.06
% 74.92/19.06
% 74.92/19.06 % ------
% 74.92/19.06 % Current options:
% 74.92/19.06 % ------
% 74.92/19.06
% 74.92/19.06
% 74.92/19.06 %
% 74.92/19.06
% 74.92/19.06 % ------ Proving...
% 74.92/19.06 % Proof_search_loop: time out after: 3139 full_loop iterations
% 74.92/19.06
% 74.92/19.06 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 74.92/19.06
% 74.92/19.06
% 74.92/19.06 % ------
% 74.92/19.06 % Current options:
% 74.92/19.06 % ------
% 74.92/19.06
% 74.92/19.06
% 74.92/19.06 %
% 74.92/19.06
% 74.92/19.06 % ------ Proving...
% 74.92/19.06 %
% 74.92/19.06
% 74.92/19.06 % SZS status Unsatisfiable for theBenchmark.p
% 74.92/19.06
% 74.92/19.06 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 74.92/19.06
% 74.92/19.06
%------------------------------------------------------------------------------