%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : BOO075-1 : TPTP v9.3.1. Released v2.6.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:00:21 PM UTC 2026
% Result : Unsatisfiable 7.91s 11.80s
% Output : CNFRefutation 7.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 2
% Syntax : Number of formulae : 62 ( 62 unt; 0 def)
% Number of atoms : 62 ( 61 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 11 ( 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 : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 125 ( 0 sgn 125 !; 0 ?; 122 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : nand(nand(X0,nand(nand(X1,X0),X0)),nand(X1,nand(X2,X0))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sh_1) ).
fof(f2,negated_conjecture,
nand(nand(a,a),nand(b,a)) != a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_meredith_2_basis_1) ).
fof(f3,plain,
a != nand(nand(a,a),nand(b,a)),
inference(reorient_equations,[],[f2]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i] : nand(nand(X0,nand(nand(X1,X0),X0)),nand(X1,nand(X2,X0))) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_52,negated_conjecture,
nand(nand(a,a),nand(b,a)) != a,
inference(cnf_transformation,[],[f3]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : nand(nand(nand(X0,nand(X1,X2)),nand(X0,nand(X0,nand(X1,X2)))),nand(nand(X2,nand(nand(X0,X2),X2)),nand(X3,nand(X0,nand(X1,X2))))) = nand(X2,nand(nand(X0,X2),X2)),
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : nand(nand(nand(X0,nand(X1,X2)),nand(nand(X3,nand(X0,nand(X1,X2))),nand(X0,nand(X1,X2)))),nand(X3,X0)) = X3,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i] : nand(nand(nand(X0,X1),nand(nand(nand(X1,nand(nand(X2,X1),X1)),nand(X0,X1)),nand(X0,X1))),X2) = nand(X1,nand(nand(X2,X1),X1)),
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] : nand(nand(nand(X0,X1),nand(nand(X2,nand(X0,X1)),nand(X0,X1))),nand(X2,X0)) = X2,
inference(superposition,[status(thm)],[c_61,c_61]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i,X2: $i] : nand(nand(X0,nand(nand(nand(nand(X0,X1),nand(nand(X2,nand(X0,X1)),nand(X0,X1))),X0),X0)),X2) = nand(nand(X0,X1),nand(nand(X2,nand(X0,X1)),nand(X0,X1))),
inference(superposition,[status(thm)],[c_61,c_62]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i] : nand(nand(X0,nand(nand(X1,X0),X0)),nand(X1,nand(X2,nand(nand(X0,X2),X2)))) = X1,
inference(superposition,[status(thm)],[c_62,c_51]) ).
tcf(c_163,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : nand(nand(nand(X0,nand(X1,X2)),nand(X0,nand(X0,nand(X1,X2)))),nand(nand(X2,nand(nand(X0,X2),X2)),nand(X3,nand(nand(nand(X0,nand(X1,X2)),X3),X3)))) = nand(X2,nand(nand(X0,X2),X2)),
inference(superposition,[status(thm)],[c_62,c_60]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i,X2: $i] : nand(nand(nand(X0,nand(X1,X2)),nand(X0,nand(X0,nand(X1,X2)))),nand(nand(X2,nand(nand(X0,X2),X2)),X0)) = nand(X2,nand(nand(X0,X2),X2)),
inference(superposition,[status(thm)],[c_61,c_60]) ).
tcf(c_353,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(nand(nand(X1,nand(nand(X1,X1),X1)),X0),X0)),X1) = nand(X1,nand(nand(X1,X1),X1)),
inference(superposition,[status(thm)],[c_51,c_132]) ).
tcf(c_354,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(nand(nand(nand(X1,nand(nand(X1,X1),X1)),nand(X1,nand(X1,nand(nand(X1,X1),X1)))),X0),X0)),nand(X1,nand(nand(X1,X1),X1))) = nand(nand(X1,nand(nand(X1,X1),X1)),nand(X1,nand(X1,nand(nand(X1,X1),X1)))),
inference(superposition,[status(thm)],[c_60,c_132]) ).
tcf(c_371,plain,
! [X0: $i,X1: $i] : nand(X0,nand(nand(X0,nand(nand(X0,X0),X0)),nand(X1,nand(X0,nand(nand(X0,X0),X0))))) = nand(X0,nand(nand(X0,X0),X0)),
inference(superposition,[status(thm)],[c_132,c_60]) ).
tcf(c_373,plain,
! [X0: $i] : nand(X0,nand(nand(X0,X0),X0)) = nand(X0,X0),
inference(superposition,[status(thm)],[c_132,c_60]) ).
tcf(c_576,plain,
! [X0: $i,X1: $i] : nand(nand(nand(X0,nand(X1,X0)),nand(X0,nand(X0,nand(X1,X0)))),X0) = nand(X0,nand(nand(X0,X0),X0)),
inference(superposition,[status(thm)],[c_51,c_163]) ).
tcf(c_638,plain,
! [X0: $i,X1: $i] : nand(nand(nand(X0,nand(X1,X0)),nand(X0,nand(X0,nand(X1,X0)))),X0) = nand(X0,X0),
inference(demodulation,[status(thm)],[c_576,c_373]) ).
tcf(c_639,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(nand(nand(X1,X1),X0),X0)),X1) = nand(X1,X1),
inference(demodulation,[status(thm)],[c_353,c_373]) ).
tcf(c_640,plain,
! [X0: $i,X1: $i] : nand(X0,nand(nand(X0,X0),nand(X1,nand(X0,X0)))) = nand(X0,X0),
inference(demodulation,[status(thm)],[c_371,c_373]) ).
tcf(c_643,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(nand(nand(nand(X1,X1),nand(X1,nand(X1,X1))),X0),X0)),nand(X1,X1)) = nand(nand(X1,X1),nand(X1,nand(X1,X1))),
inference(demodulation,[status(thm)],[c_354,c_373]) ).
tcf(c_1293,plain,
! [X0: $i,X1: $i] : nand(nand(X0,X0),nand(X0,nand(X1,X0))) = X0,
inference(superposition,[status(thm)],[c_373,c_51]) ).
tcf(c_1296,plain,
! [X0: $i] : nand(nand(X0,X0),nand(X0,X0)) = X0,
inference(superposition,[status(thm)],[c_373,c_51]) ).
tcf(c_1394,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(nand(X1,X0),X0)),nand(X1,X1)) = X1,
inference(superposition,[status(thm)],[c_640,c_132]) ).
tcf(c_1534,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(nand(nand(nand(X0,X0),nand(nand(nand(X0,X0),nand(X0,nand(X0,X0))),nand(X0,X0))),X0),X0)),nand(X1,nand(nand(nand(nand(X0,X0),nand(X0,nand(X0,X0))),X1),X1))) = nand(nand(X0,X0),nand(nand(nand(X0,X0),nand(X0,nand(X0,X0))),nand(X0,X0))),
inference(superposition,[status(thm)],[c_643,c_130]) ).
tcf(c_1705,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(nand(X0,X0),X0)),nand(X1,nand(nand(X0,X1),X1))) = X0,
inference(demodulation,[status(thm)],[c_1534,c_1293]) ).
tcf(c_1706,plain,
! [X0: $i,X1: $i] : nand(nand(X0,X0),nand(X1,nand(nand(X0,X1),X1))) = X0,
inference(demodulation,[status(thm)],[c_1705,c_373]) ).
tcf(c_2383,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(nand(nand(nand(X0,nand(X1,X0)),nand(X0,nand(X0,nand(X1,X0)))),X0),X0)),nand(X0,X0)) = nand(nand(X0,nand(X1,X0)),nand(X0,nand(X0,nand(X1,X0)))),
inference(superposition,[status(thm)],[c_1293,c_130]) ).
tcf(c_2445,plain,
! [X0: $i,X1: $i] : nand(nand(nand(X0,nand(nand(X1,X0),X0)),nand(X0,nand(X0,nand(nand(X1,X0),X0)))),nand(nand(X0,nand(nand(X0,X0),X0)),nand(nand(X1,X1),nand(X1,nand(X1,X1))))) = nand(X0,nand(nand(X0,X0),X0)),
inference(superposition,[status(thm)],[c_1394,c_163]) ).
tcf(c_2450,plain,
! [X0: $i,X1: $i] : nand(X0,nand(X1,nand(nand(nand(X0,X0),X1),X1))) = nand(X0,X0),
inference(superposition,[status(thm)],[c_1296,c_1706]) ).
tcf(c_2586,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(X1,X0)),nand(X0,nand(X0,nand(X1,X0)))) = X0,
inference(demodulation,[status(thm)],[c_2383,c_373,c_638,c_1296]) ).
tcf(c_2588,plain,
! [X0: $i,X1: $i] : nand(X0,nand(nand(X0,nand(nand(X0,X0),X0)),nand(nand(X1,X1),nand(X1,nand(X1,X1))))) = nand(X0,nand(nand(X0,X0),X0)),
inference(demodulation,[status(thm)],[c_2445,c_2586]) ).
tcf(c_2589,plain,
! [X0: $i,X1: $i] : nand(X0,nand(nand(X0,X0),X1)) = nand(X0,X0),
inference(demodulation,[status(thm)],[c_2588,c_373,c_1293]) ).
tcf(c_3210,plain,
! [X0: $i,X1: $i] : nand(nand(X0,X0),nand(X0,X1)) = X0,
inference(superposition,[status(thm)],[c_1296,c_2589]) ).
tcf(c_3266,plain,
! [X0: $i,X1: $i] : nand(nand(nand(nand(nand(X0,X0),nand(X0,X0)),X1),nand(nand(nand(X0,X0),nand(X0,X0)),nand(nand(nand(X0,X0),nand(X0,X0)),X1))),X0) = nand(X0,X0),
inference(superposition,[status(thm)],[c_2589,c_639]) ).
tcf(c_3280,plain,
! [X0: $i,X1: $i] : nand(X0,nand(nand(nand(nand(X0,X0),nand(X0,X0)),X1),nand(nand(nand(X0,X0),nand(X0,X0)),nand(nand(nand(X0,X0),nand(X0,X0)),X1)))) = nand(X0,X0),
inference(superposition,[status(thm)],[c_2589,c_2450]) ).
tcf(c_3351,plain,
! [X0: $i] : nand(nand(X0,nand(nand(nand(X0,X0),X0),X0)),nand(X0,X0)) = X0,
inference(superposition,[status(thm)],[c_2450,c_2586]) ).
tcf(c_3360,plain,
! [X0: $i,X1: $i] : nand(nand(nand(X0,X1),X0),nand(nand(X0,X1),nand(nand(X0,X1),X0))) = nand(X0,X1),
inference(superposition,[status(thm)],[c_85,c_2586]) ).
tcf(c_3413,plain,
! [X0: $i,X1: $i] : nand(X0,nand(nand(X0,nand(X1,X0)),X0)) = nand(X0,nand(X1,X0)),
inference(superposition,[status(thm)],[c_2586,c_2586]) ).
tcf(c_3522,plain,
! [X0: $i,X1: $i] : nand(X0,nand(nand(X0,X1),nand(X0,nand(X0,X1)))) = nand(X0,X0),
inference(demodulation,[status(thm)],[c_3280,c_3210]) ).
tcf(c_3523,plain,
! [X0: $i,X1: $i] : nand(nand(nand(X0,X1),nand(X0,nand(X0,X1))),X0) = nand(X0,X0),
inference(demodulation,[status(thm)],[c_3266,c_3210]) ).
tcf(c_3607,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(nand(X0,X0),X0)),nand(nand(nand(X0,nand(nand(X0,X0),X0)),nand(X0,nand(X0,nand(nand(X0,X0),X0)))),X1)) = nand(nand(X0,nand(nand(X0,X0),X0)),nand(X0,nand(X0,nand(nand(X0,X0),X0)))),
inference(superposition,[status(thm)],[c_60,c_3210]) ).
tcf(c_3659,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(nand(nand(nand(X0,X1),nand(X0,nand(X0,X1))),X0),X0)),nand(X0,X0)) = nand(nand(X0,X1),nand(X0,nand(X0,X1))),
inference(superposition,[status(thm)],[c_3210,c_130]) ).
tcf(c_3711,plain,
! [X0: $i,X1: $i] : nand(nand(nand(nand(X0,X0),nand(X1,X0)),nand(nand(X0,X0),nand(nand(X0,X0),nand(X1,X0)))),X0) = nand(X0,nand(nand(nand(X0,X0),X0),X0)),
inference(superposition,[status(thm)],[c_3351,c_164]) ).
tcf(c_3718,plain,
! [X0: $i] : nand(X0,nand(nand(nand(X0,X0),X0),X0)) = nand(X0,nand(X0,X0)),
inference(superposition,[status(thm)],[c_639,c_3413]) ).
tcf(c_3741,plain,
! [X0: $i,X1: $i] : nand(nand(nand(nand(X0,nand(X1,X0)),X0),nand(nand(X0,nand(X1,X0)),nand(nand(X0,nand(X1,X0)),X0))),nand(X0,X0)) = X0,
inference(superposition,[status(thm)],[c_3413,c_1394]) ).
tcf(c_3774,plain,
! [X0: $i,X1: $i] : nand(nand(nand(nand(nand(X0,X0),nand(X1,nand(X0,X0))),nand(X0,X0)),nand(nand(nand(X0,X0),nand(X1,nand(X0,X0))),nand(nand(nand(X0,X0),nand(X1,nand(X0,X0))),nand(X0,X0)))),X0) = nand(X0,X0),
inference(superposition,[status(thm)],[c_3413,c_639]) ).
tcf(c_3847,plain,
! [X0: $i,X1: $i,X2: $i] : nand(nand(nand(X0,X0),nand(nand(nand(nand(nand(X0,X1),nand(X0,nand(X0,X1))),nand(nand(X2,nand(nand(X0,X1),nand(X0,nand(X0,X1)))),nand(nand(X0,X1),nand(X0,nand(X0,X1))))),nand(X0,X0)),nand(X0,X0))),X2) = nand(nand(nand(X0,X1),nand(X0,nand(X0,X1))),nand(nand(X2,nand(nand(X0,X1),nand(X0,nand(X0,X1)))),nand(nand(X0,X1),nand(X0,nand(X0,X1))))),
inference(superposition,[status(thm)],[c_3522,c_62]) ).
tcf(c_3850,plain,
! [X0: $i,X1: $i] : nand(nand(nand(X0,X1),nand(nand(nand(nand(nand(X0,X1),nand(X0,nand(X0,X1))),nand(nand(X0,X0),nand(nand(X0,X1),nand(X0,nand(X0,X1))))),nand(X0,X1)),nand(X0,X1))),X0) = nand(nand(nand(X0,X1),nand(X0,nand(X0,X1))),nand(nand(X0,X0),nand(nand(X0,X1),nand(X0,nand(X0,X1))))),
inference(superposition,[status(thm)],[c_3522,c_130]) ).
tcf(c_3927,plain,
! [X0: $i,X1: $i,X2: $i] : nand(nand(nand(nand(X0,X1),nand(X0,nand(X0,X1))),nand(nand(nand(nand(X0,X0),nand(nand(X2,nand(X0,X0)),nand(X0,X0))),nand(nand(X0,X1),nand(X0,nand(X0,X1)))),nand(nand(X0,X1),nand(X0,nand(X0,X1))))),X2) = nand(nand(X0,X0),nand(nand(X2,nand(X0,X0)),nand(X0,X0))),
inference(superposition,[status(thm)],[c_3523,c_130]) ).
tcf(c_3942,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(X1,X0)),nand(X0,X0)) = X0,
inference(demodulation,[status(thm)],[c_3741,c_3360]) ).
tcf(c_3944,plain,
! [X0: $i,X1: $i] : nand(nand(X0,X1),nand(X0,nand(X0,X1))) = X0,
inference(demodulation,[status(thm)],[c_3659,c_3942]) ).
tcf(c_3947,plain,
! [X0: $i] : nand(nand(X0,X0),X0) = nand(X0,nand(X0,X0)),
inference(demodulation,[status(thm)],[c_3711,c_3718,c_3944]) ).
tcf(c_3978,plain,
! [X0: $i,X1: $i] : nand(nand(nand(X0,X0),nand(X1,nand(X0,X0))),X0) = nand(X0,X0),
inference(demodulation,[status(thm)],[c_3774,c_3944]) ).
tcf(c_3986,plain,
! [X0: $i,X1: $i] : nand(nand(X0,nand(X0,nand(X0,X0))),nand(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_3607,c_3944,c_3947]) ).
tcf(c_4008,plain,
! [X0: $i,X1: $i] : nand(nand(X0,X0),nand(nand(X1,nand(X0,X0)),nand(X0,X0))) = nand(nand(X0,nand(X0,nand(X0,X0))),X1),
inference(demodulation,[status(thm)],[c_3927,c_3944,c_3947,c_3978]) ).
tcf(c_4015,plain,
! [X0: $i] : nand(X0,nand(X0,nand(X0,X0))) = nand(X0,X0),
inference(demodulation,[status(thm)],[c_3850,c_3944,c_3947,c_3986]) ).
tcf(c_4042,plain,
! [X0: $i,X1: $i] : nand(nand(nand(X0,X0),nand(X0,nand(nand(X1,X0),X0))),X1) = nand(X0,nand(nand(X1,X0),X0)),
inference(demodulation,[status(thm)],[c_3847,c_3944,c_4008,c_4015]) ).
tcf(c_4043,plain,
! [X0: $i,X1: $i] : nand(X0,nand(nand(X1,X0),X0)) = nand(X0,X1),
inference(demodulation,[status(thm)],[c_4042,c_3210]) ).
tcf(c_4079,plain,
! [X0: $i,X1: $i] : nand(nand(X0,X0),nand(X1,X0)) = X0,
inference(demodulation,[status(thm)],[c_1706,c_4043]) ).
tcf(c_4093,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_52,c_4079]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO075-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/10.39 % Computer : n010.cluster.edu
% 0.13/10.39 % Model : x86_64 x86_64
% 0.13/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.39 % Memory : 8046.5625MB
% 0.13/10.39 % OS : Linux 6.8.0-71-generic
% 0.13/10.39 % CPULimit : 300
% 0.13/10.39 % WCLimit : 300
% 0.13/10.39 % DateTime : Fri Sep 25 06:44:30 UTC 2026
% 0.17/10.40 % CPUTime :
% 0.17/10.40 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.17/10.43 Running UEQ theorem proving
% 0.17/10.43 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/10.45
% 0.17/10.45 % ======== iProver multi-core TPTP/SMT =========
% 0.17/10.45
% 0.17/10.45 % Detected problem language: tptp
% 0.17/10.46 % Proving...
% 7.91/11.80 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 7.91/11.80 % SZS status Started for theBenchmark.p
% 7.91/11.80 % SZS status Unsatisfiable for theBenchmark.p
% 7.91/11.80
% 7.91/11.80 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.91/11.80
% 7.91/11.80 % ------ iProver source info
% 7.91/11.80
% 7.91/11.80 % git: date: 2026-07-19 20:42:38 +0200
% 7.91/11.80 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.91/11.80 % git: non_committed_changes: false
% 7.91/11.80
% 7.91/11.80 % ------ Parsing...% successful
% 7.91/11.80
% 7.91/11.80
% 7.91/11.80 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 7.91/11.80 % ------ Proving...
% 7.91/11.80 % ------ Problem Properties
% 7.91/11.80
% 7.91/11.80 %
% 7.91/11.80 % clauses 2
% 7.91/11.80 % conjectures 1
% 7.91/11.80 % EPR 0
% 7.91/11.80 % Horn 2
% 7.91/11.80 % unary 2
% 7.91/11.80 % binary 0
% 7.91/11.80 % lits 2
% 7.91/11.80 % lits eq 2
% 7.91/11.80 % fd_pure 0
% 7.91/11.80 % fd_pseudo 0
% 7.91/11.80 % fd_cond 0
% 7.91/11.80 % fd_pseudo_cond 0
% 7.91/11.80 % AC symbols 0
% 7.91/11.80
% 7.91/11.80 % ------ Input Options Time Limit: Unbounded
% 7.91/11.80
% 7.91/11.80
% 7.91/11.80 % ------
% 7.91/11.80 % Current options:
% 7.91/11.80 % ------
% 7.91/11.80
% 7.91/11.80
% 7.91/11.80 %
% 7.91/11.80
% 7.91/11.80 % ------ Proving...
% 7.91/11.80 %
% 7.91/11.80
% 7.91/11.80 % SZS status Unsatisfiable for theBenchmark.p
% 7.91/11.80
% 7.91/11.80 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 7.91/11.80
% 7.91/11.80
%------------------------------------------------------------------------------