%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT154-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n011.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:18 PM UTC 2026
% Result : Unsatisfiable 125.95s 22.93s
% Output : CNFRefutation 125.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 23
% Syntax : Number of formulae : 106 ( 106 unt; 14 def)
% Number of atoms : 277 ( 105 equ)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 14 usr; 15 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 80 ( 0 sgn 80 !; 0 ?; 61 :)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-0.ax',idempotence_of_join) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-0.ax',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-0.ax',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/LAT001-0.ax',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/LAT001-0.ax',associativity_of_join) ).
fof(f9,axiom,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,X3)))) = meet(X0,join(X1,meet(X2,join(X1,join(X3,meet(X0,X2)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H42) ).
fof(f10,negated_conjecture,
meet(a,join(b,meet(a,c))) != meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_H6) ).
tcf(c_60,plain,
! [X0: $i] : join(X0,X0) = X0,
inference(cnf_transformation,[],[f2]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[],[f3]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] : join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] : meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[],[f5]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f6]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[],[f8]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : meet(X0,join(X1,meet(X2,join(X1,join(X3,meet(X0,X2)))))) = meet(X0,join(X1,meet(X2,join(X0,X3)))),
inference(cnf_transformation,[],[f9]) ).
tcf(c_68,negated_conjecture,
meet(a,join(meet(a,join(b,meet(a,c))),meet(c,join(a,b)))) != meet(a,join(b,meet(a,c))),
inference(cnf_transformation,[],[f10]) ).
tcf(c_78,negated_conjecture,
meet(a,join(meet(c,join(a,b)),meet(a,join(b,meet(a,c))))) != meet(a,join(b,meet(a,c))),
inference(theory_normalisation,[status(thm)],[c_68,c_65,c_63,c_66,c_64]) ).
tcf(c_103,definition,
iPr_def_10 = join(a,b),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_104,definition,
iPr_def_11 = meet(c,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_105,definition,
iPr_def_12 = meet(a,c),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_106,definition,
iPr_def_13 = join(b,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_107,definition,
iPr_def_14 = meet(a,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_108,definition,
iPr_def_15 = join(iPr_def_11,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_109,definition,
iPr_def_16 = meet(a,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_110,negated_conjecture,
iPr_def_16 != iPr_def_14,
inference(demodulation,[status(thm)],[c_78,c_105,c_106,c_107,c_103,c_104,c_108,c_109]) ).
tcf(c_111,definition,
iPr_def_17 = meet(a,c),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_112,definition,
iPr_def_18 = join(b,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_113,definition,
iPr_def_19 = meet(a,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_114,definition,
iPr_def_20 = join(a,b),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_115,definition,
iPr_def_21 = meet(c,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_116,definition,
iPr_def_22 = join(iPr_def_11,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_117,definition,
iPr_def_23 = meet(a,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_118,negated_conjecture,
iPr_def_16 != iPr_def_14,
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_119,plain,
iPr_def_12 = iPr_def_17,
inference(demodulation,[status(thm)],[c_105,c_111]) ).
tcf(c_120,plain,
iPr_def_13 = iPr_def_18,
inference(demodulation,[status(thm)],[c_106,c_112]) ).
tcf(c_121,plain,
iPr_def_14 = iPr_def_19,
inference(demodulation,[status(thm)],[c_107,c_113]) ).
tcf(c_122,plain,
iPr_def_10 = iPr_def_20,
inference(demodulation,[status(thm)],[c_103,c_114]) ).
tcf(c_123,plain,
iPr_def_11 = iPr_def_21,
inference(demodulation,[status(thm)],[c_104,c_115]) ).
tcf(c_124,plain,
iPr_def_15 = iPr_def_22,
inference(demodulation,[status(thm)],[c_108,c_116]) ).
tcf(c_125,plain,
iPr_def_16 = iPr_def_23,
inference(demodulation,[status(thm)],[c_109,c_117]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(demodulation,[status(thm)],[c_66]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i,X2: $i] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(demodulation,[status(thm)],[c_65]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i] : meet(X0,X1) = meet(X1,X0),
inference(demodulation,[status(thm)],[c_63]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i] : join(X0,meet(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_62]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i] : meet(X0,join(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_61]) ).
tcf(c_132,plain,
! [X0: $i] : join(X0,X0) = X0,
inference(demodulation,[status(thm)],[c_60]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : meet(X0,join(X1,meet(X2,join(X1,join(X3,meet(X0,X2)))))) = meet(X0,join(X1,meet(X2,join(X0,X3)))),
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_289,plain,
! [X0: $i,X1: $i] : meet(X0,join(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_128,c_131]) ).
tcf(c_676,plain,
! [X0: $i,X1: $i,X2: $i] : meet(X0,join(X1,join(X2,X0))) = X0,
inference(superposition,[status(thm)],[c_126,c_289]) ).
tcf(c_1201,plain,
meet(a,c) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_111,c_119]) ).
tcf(c_1203,plain,
join(b,iPr_def_12) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_112,c_120]) ).
tcf(c_1204,plain,
join(iPr_def_12,b) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_1203,c_126,c_128,c_127,c_129]) ).
tcf(c_1205,plain,
! [X0: $i] : join(iPr_def_12,join(b,X0)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_1204,c_126]) ).
tcf(c_1206,plain,
meet(a,iPr_def_13) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_113,c_121]) ).
tcf(c_1207,plain,
meet(iPr_def_13,a) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_1206,c_126,c_128,c_127,c_129]) ).
tcf(c_1208,plain,
! [X0: $i] : meet(iPr_def_13,meet(a,X0)) = meet(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_1207,c_127]) ).
tcf(c_1209,plain,
join(a,b) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_114,c_122]) ).
tcf(c_1211,plain,
meet(c,iPr_def_10) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_115,c_123]) ).
tcf(c_1212,plain,
meet(iPr_def_10,c) = iPr_def_11,
inference(theory_normalisation,[status(thm)],[c_1211,c_126,c_128,c_127,c_129]) ).
tcf(c_1214,plain,
join(iPr_def_11,iPr_def_14) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_116,c_124]) ).
tcf(c_1215,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_14,X0)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_1214,c_126]) ).
tcf(c_1216,plain,
meet(a,iPr_def_15) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_117,c_125]) ).
tcf(c_1217,plain,
meet(iPr_def_15,a) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_1216,c_126,c_128,c_127,c_129]) ).
tcf(c_1218,plain,
! [X0: $i] : meet(iPr_def_15,meet(a,X0)) = meet(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_1217,c_127]) ).
tcf(c_1223,plain,
join(iPr_def_12,b) = join(iPr_def_13,b),
inference(superposition,[status(thm)],[c_132,c_1205]) ).
tcf(c_1224,plain,
! [X0: $i] : join(iPr_def_12,join(X0,b)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_128,c_1205]) ).
tcf(c_1227,plain,
join(iPr_def_13,b) = iPr_def_13,
inference(demodulation,[status(thm)],[c_1223,c_1204]) ).
tcf(c_1230,plain,
! [X0: $i] : join(iPr_def_13,join(b,X0)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_1227,c_126]) ).
tcf(c_1231,plain,
meet(iPr_def_13,iPr_def_12) = meet(iPr_def_14,c),
inference(superposition,[status(thm)],[c_1201,c_1208]) ).
tcf(c_1234,plain,
meet(iPr_def_12,iPr_def_13) = meet(iPr_def_14,c),
inference(theory_normalisation,[status(thm)],[c_1231,c_126,c_128,c_127,c_129]) ).
tcf(c_1251,plain,
join(a,iPr_def_12) = a,
inference(superposition,[status(thm)],[c_1201,c_130]) ).
tcf(c_1253,plain,
! [X0: $i,X1: $i] : join(X0,meet(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_129,c_130]) ).
tcf(c_1257,plain,
join(iPr_def_13,iPr_def_14) = iPr_def_13,
inference(superposition,[status(thm)],[c_1207,c_130]) ).
tcf(c_1260,plain,
join(iPr_def_15,iPr_def_16) = iPr_def_15,
inference(superposition,[status(thm)],[c_1217,c_130]) ).
tcf(c_1266,plain,
join(iPr_def_12,a) = a,
inference(theory_normalisation,[status(thm)],[c_1251,c_126,c_128,c_127,c_129]) ).
tcf(c_1277,plain,
! [X0: $i,X1: $i] : meet(X0,join(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_128,c_131]) ).
tcf(c_1280,plain,
meet(iPr_def_12,iPr_def_13) = iPr_def_12,
inference(superposition,[status(thm)],[c_1204,c_131]) ).
tcf(c_1295,plain,
meet(iPr_def_14,c) = iPr_def_12,
inference(demodulation,[status(thm)],[c_1234,c_1280]) ).
tcf(c_1319,plain,
! [X0: $i,X1: $i] : meet(a,join(X0,meet(c,join(X0,join(X1,iPr_def_12))))) = meet(a,join(X0,meet(c,join(a,X1)))),
inference(superposition,[status(thm)],[c_1201,c_134]) ).
tcf(c_1361,plain,
join(iPr_def_14,iPr_def_12) = iPr_def_14,
inference(superposition,[status(thm)],[c_1295,c_130]) ).
tcf(c_1363,plain,
join(iPr_def_12,iPr_def_14) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_1361,c_126,c_128,c_127,c_129]) ).
tcf(c_1368,plain,
! [X0: $i] : join(iPr_def_12,join(iPr_def_14,X0)) = join(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_1363,c_126]) ).
tcf(c_1388,plain,
join(iPr_def_13,iPr_def_12) = iPr_def_13,
inference(superposition,[status(thm)],[c_1280,c_1253]) ).
tcf(c_1401,plain,
join(iPr_def_12,iPr_def_13) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_1388,c_126,c_128,c_127,c_129]) ).
tcf(c_1434,plain,
! [X0: $i] : meet(iPr_def_16,join(X0,iPr_def_15)) = iPr_def_16,
inference(superposition,[status(thm)],[c_1260,c_676]) ).
tcf(c_1650,plain,
meet(iPr_def_14,iPr_def_15) = iPr_def_14,
inference(superposition,[status(thm)],[c_1214,c_1277]) ).
tcf(c_1962,plain,
! [X0: $i] : meet(iPr_def_16,join(iPr_def_15,X0)) = iPr_def_16,
inference(superposition,[status(thm)],[c_128,c_1434]) ).
tcf(c_6812,plain,
join(iPr_def_13,iPr_def_14) = join(iPr_def_14,b),
inference(superposition,[status(thm)],[c_1368,c_1224]) ).
tcf(c_6816,plain,
join(iPr_def_14,b) = iPr_def_13,
inference(demodulation,[status(thm)],[c_6812,c_1257]) ).
tcf(c_6836,plain,
join(iPr_def_11,iPr_def_13) = join(iPr_def_15,b),
inference(superposition,[status(thm)],[c_6816,c_1215]) ).
tcf(c_7332,plain,
meet(iPr_def_16,join(iPr_def_11,iPr_def_13)) = iPr_def_16,
inference(superposition,[status(thm)],[c_6836,c_1962]) ).
tcf(c_7530,plain,
meet(a,join(iPr_def_13,meet(c,join(a,b)))) = meet(a,join(iPr_def_13,meet(c,join(iPr_def_13,iPr_def_12)))),
inference(superposition,[status(thm)],[c_1230,c_1319]) ).
tcf(c_7538,plain,
! [X0: $i] : meet(a,join(X0,meet(c,join(X0,iPr_def_12)))) = meet(a,join(X0,meet(c,join(a,iPr_def_12)))),
inference(superposition,[status(thm)],[c_132,c_1319]) ).
tcf(c_7571,plain,
! [X0: $i] : meet(a,join(X0,meet(c,join(X0,iPr_def_12)))) = meet(a,join(X0,meet(c,join(iPr_def_12,a)))),
inference(theory_normalisation,[status(thm)],[c_7538,c_126,c_128,c_127,c_129]) ).
tcf(c_7572,plain,
! [X0: $i] : meet(a,join(X0,meet(c,join(X0,iPr_def_12)))) = meet(a,join(X0,iPr_def_12)),
inference(demodulation,[status(thm)],[c_7571,c_129,c_1201,c_1266]) ).
tcf(c_7582,plain,
meet(a,join(iPr_def_13,meet(c,join(a,b)))) = meet(a,join(iPr_def_13,iPr_def_12)),
inference(demodulation,[status(thm)],[c_7530,c_7572]) ).
tcf(c_7583,plain,
meet(a,join(iPr_def_13,meet(c,join(a,b)))) = meet(a,join(iPr_def_12,iPr_def_13)),
inference(theory_normalisation,[status(thm)],[c_7582,c_126,c_128,c_127,c_129]) ).
tcf(c_7584,plain,
meet(a,join(iPr_def_11,iPr_def_13)) = iPr_def_14,
inference(demodulation,[status(thm)],[c_7583,c_129,c_128,c_1207,c_1209,c_1212,c_1401]) ).
tcf(c_7629,plain,
meet(iPr_def_16,join(iPr_def_11,iPr_def_13)) = meet(iPr_def_15,iPr_def_14),
inference(superposition,[status(thm)],[c_7584,c_1218]) ).
tcf(c_7632,plain,
meet(iPr_def_16,join(iPr_def_11,iPr_def_13)) = meet(iPr_def_14,iPr_def_15),
inference(theory_normalisation,[status(thm)],[c_7629,c_126,c_128,c_127,c_129]) ).
tcf(c_7633,plain,
iPr_def_14 = iPr_def_16,
inference(demodulation,[status(thm)],[c_7632,c_1650,c_7332]) ).
tcf(c_7856,plain,
iPr_def_14 != iPr_def_14,
inference(demodulation,[status(thm)],[c_118,c_7633]) ).
tcf(c_7858,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_7856]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT154-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 20:23:58 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running UEQ theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 125.95/22.93 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 125.95/22.93 % SZS status Started for theBenchmark.p
% 125.95/22.93 % SZS status Unsatisfiable for theBenchmark.p
% 125.95/22.93
% 125.95/22.93 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 125.95/22.93
% 125.95/22.93 % ------ iProver source info
% 125.95/22.93
% 125.95/22.93 % git: date: 2026-07-19 20:42:38 +0200
% 125.95/22.93 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 125.95/22.93 % git: non_committed_changes: false
% 125.95/22.93
% 125.95/22.93 % ------ Parsing...% successful
% 125.95/22.93
% 125.95/22.93
% 125.95/22.93 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 125.95/22.93
% 125.95/22.93 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 125.95/22.93
% 125.95/22.93 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 125.95/22.93
% 125.95/22.93 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 125.95/22.93 % ------ Proving...
% 125.95/22.93 % ------ Problem Properties
% 125.95/22.93
% 125.95/22.93 %
% 125.95/22.93 % clauses 24
% 125.95/22.93 % conjectures 1
% 125.95/22.93 % EPR 8
% 125.95/22.93 % Horn 24
% 125.95/22.93 % unary 24
% 125.95/22.93 % binary 0
% 125.95/22.93 % lits 24
% 125.95/22.93 % lits eq 24
% 125.95/22.93 % fd_pure 0
% 125.95/22.93 % fd_pseudo 0
% 125.95/22.93 % fd_cond 0
% 125.95/22.93 % fd_pseudo_cond 0
% 125.95/22.93 % AC symbols 2
% 125.95/22.93
% 125.95/22.93 % ------ Input Options Time Limit: Unbounded
% 125.95/22.93
% 125.95/22.93
% 125.95/22.93 % ------
% 125.95/22.93 % Current options:
% 125.95/22.93 % ------
% 125.95/22.93
% 125.95/22.93
% 125.95/22.93 %
% 125.95/22.93
% 125.95/22.93 % ------ Proving...
% 125.95/22.93 %
% 125.95/22.93
% 125.95/22.93 % SZS status Unsatisfiable for theBenchmark.p
% 125.95/22.93
% 125.95/22.93 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 125.95/22.93
% 125.95/22.93
%------------------------------------------------------------------------------