%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HEN007-2 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:28:32 PM UTC 2026
% Result : Unsatisfiable 0.31s 1.62s
% Output : CNFRefutation 0.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 35
% Syntax : Number of clauses : 118 ( 73 unt; 0 nHn; 80 RR)
% Number of literals : 207 ( 45 equ; 118 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 7 con; 0-2 aty)
% Number of variables : 203 ( 24 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(quotient_property,axiom,
( less_equal(X7,X8)
| ~ quotient(X1,X2,X3)
| ~ quotient(X2,X4,X5)
| ~ quotient(X1,X4,X6)
| ~ quotient(X6,X5,X7)
| ~ quotient(X3,X4,X8) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',quotient_property) ).
cnf(xQyLEz_implies_xQzLEy,axiom,
( less_equal(X5,X2)
| ~ quotient(X1,X2,X3)
| ~ less_equal(X3,X4)
| ~ quotient(X1,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xQyLEz_implies_xQzLEy) ).
cnf(well_defined,axiom,
( X3 = X4
| ~ quotient(X1,X2,X3)
| ~ quotient(X1,X2,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',well_defined) ).
cnf(divisor_existence,axiom,
( less_equal(X3,X1)
| ~ quotient(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',divisor_existence) ).
cnf(less_equal_quotient,axiom,
( less_equal(X1,X2)
| ~ quotient(X1,X2,zero) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',less_equal_quotient) ).
cnf(closure,axiom,
quotient(X1,X2,divide(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',closure) ).
cnf(quotient_less_equal,axiom,
( quotient(X1,X2,zero)
| ~ less_equal(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',quotient_less_equal) ).
cnf(transitivity_of_less_equal,axiom,
( less_equal(X1,X3)
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_less_equal) ).
cnf(x_divde_zero_is_x,axiom,
quotient(X1,zero,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_divde_zero_is_x) ).
cnf(x_divide_x_is_zero,axiom,
quotient(X1,X1,zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_divide_x_is_zero) ).
cnf(zero_divide_anything_is_zero,axiom,
quotient(zero,X1,zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',zero_divide_anything_is_zero) ).
cnf(everything_divide_identity_is_zero,axiom,
quotient(X1,identity,zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',everything_divide_identity_is_zero) ).
cnf(zQy,hypothesis,
quotient(z,y,zQy),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',zQy) ).
cnf(zQx,hypothesis,
quotient(z,x,zQx),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',zQx) ).
cnf(less_equal_and_equal,axiom,
( X1 = X2
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',less_equal_and_equal) ).
cnf(prove_zQyLEzQx,negated_conjecture,
~ less_equal(zQy,zQx),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_zQyLEzQx) ).
cnf(zero_is_smallest,axiom,
less_equal(zero,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',zero_is_smallest) ).
cnf(identity_is_largest,axiom,
less_equal(X1,identity),
file('/export/starexec/sandbox2/benchmark/Axioms/HEN001-0.ax',identity_is_largest) ).
cnf(xLEy,hypothesis,
less_equal(x,y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xLEy) ).
cnf(i_0_19,axiom,
( less_equal(X7,X8)
| ~ quotient(X1,X2,X3)
| ~ quotient(X2,X4,X5)
| ~ quotient(X1,X4,X6)
| ~ quotient(X6,X5,X7)
| ~ quotient(X3,X4,X8) ),
quotient_property,
[final] ).
cnf(i_0_20,axiom,
( less_equal(X5,X2)
| ~ quotient(X1,X2,X3)
| ~ less_equal(X3,X4)
| ~ quotient(X1,X4,X5) ),
xQyLEz_implies_xQzLEy,
[final] ).
cnf(i_0_21,axiom,
( X3 = X4
| ~ quotient(X1,X2,X3)
| ~ quotient(X1,X2,X4) ),
well_defined,
[final] ).
cnf(i_0_22,axiom,
( less_equal(X3,X1)
| ~ quotient(X1,X2,X3) ),
divisor_existence,
[final] ).
cnf(i_0_23,axiom,
( less_equal(X1,X2)
| ~ quotient(X1,X2,zero) ),
less_equal_quotient,
[final] ).
cnf(i_0_24,axiom,
quotient(X1,X2,divide(X1,X2)),
closure,
[final] ).
cnf(i_0_25,axiom,
( quotient(X1,X2,zero)
| ~ less_equal(X1,X2) ),
quotient_less_equal,
[final] ).
cnf(i_0_26,axiom,
( less_equal(X1,X3)
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X3) ),
transitivity_of_less_equal,
[final] ).
cnf(i_0_27,axiom,
quotient(X1,zero,X1),
x_divde_zero_is_x,
[final] ).
cnf(i_0_28,axiom,
quotient(X1,X1,zero),
x_divide_x_is_zero,
[final] ).
cnf(i_0_29,axiom,
quotient(zero,X1,zero),
zero_divide_anything_is_zero,
[final] ).
cnf(i_0_30,axiom,
quotient(X1,identity,zero),
everything_divide_identity_is_zero,
[final] ).
cnf(i_0_31,hypothesis,
quotient(z,y,zQy),
zQy,
[final] ).
cnf(i_0_32,hypothesis,
quotient(z,x,zQx),
zQx,
[final] ).
cnf(i_0_33,axiom,
( X1 = X2
| ~ less_equal(X1,X2)
| ~ less_equal(X2,X1) ),
less_equal_and_equal,
[final] ).
cnf(i_0_34,negated_conjecture,
~ less_equal(zQy,zQx),
prove_zQyLEzQx,
[final] ).
cnf(i_0_35,axiom,
less_equal(zero,X1),
zero_is_smallest,
[final] ).
cnf(i_0_36,axiom,
less_equal(X1,identity),
identity_is_largest,
[final] ).
cnf(i_0_37,hypothesis,
less_equal(x,y),
xLEy,
[final] ).
cnf(i_0_38,axiom,
X1 = X1 ).
cnf(i_0_39,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_40,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_41,axiom,
( X1 != X2
| ~ less_equal(X1,X3)
| less_equal(X2,X3) ) ).
cnf(i_0_42,axiom,
( X1 != X2
| ~ less_equal(X3,X1)
| less_equal(X3,X2) ) ).
cnf(i_0_43,axiom,
( X1 != X2
| ~ quotient(X1,X3,X4)
| quotient(X2,X3,X4) ) ).
cnf(i_0_44,axiom,
( X1 != X2
| ~ quotient(X3,X1,X4)
| quotient(X3,X2,X4) ) ).
cnf(i_0_45,axiom,
( X1 != X2
| ~ quotient(X3,X4,X1)
| quotient(X3,X4,X2) ) ).
cnf(i_0_38_001,axiom,
X1 = X1 ).
cnf(i_0_39_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_40_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_41_004,axiom,
( X1 != X2
| ~ less_equal(X1,X3)
| less_equal(X2,X3) ) ).
cnf(i_0_42_005,axiom,
( X1 != X2
| ~ less_equal(X3,X1)
| less_equal(X3,X2) ) ).
cnf(i_0_43_006,axiom,
( X1 != X2
| ~ quotient(X1,X3,X4)
| quotient(X2,X3,X4) ) ).
cnf(i_0_44_007,axiom,
( X1 != X2
| ~ quotient(X3,X1,X4)
| quotient(X3,X2,X4) ) ).
cnf(i_0_45_008,axiom,
( X1 != X2
| ~ quotient(X3,X4,X1)
| quotient(X3,X4,X2) ) ).
cnf(i_0_46,plain,
~ quotient(zQx,X1,zQy),
inference(scs_inference,[],[i_0_34,i_0_22]) ).
cnf(i_0_47,plain,
( less_equal(X1,X2)
| ~ quotient(X2,X3,X1) ),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_48,plain,
less_equal(X1,X1),
inference(scs_inference,[],[i_0_34,i_0_28,i_0_22,i_0_23]) ).
cnf(i_0_49,plain,
( ~ quotient(X1,X2,zero)
| less_equal(X1,X2) ),
inference(rename_variables,[],[i_0_23]) ).
cnf(i_0_50,plain,
~ less_equal(zQy,zero),
inference(scs_inference,[],[i_0_34,i_0_28,i_0_35,i_0_22,i_0_23,i_0_26]) ).
cnf(i_0_51,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_52,plain,
( ~ less_equal(X1,X2)
| less_equal(X3,X2)
| ~ less_equal(X3,X1) ),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_53,plain,
zero != zQy,
inference(scs_inference,[],[i_0_34,i_0_28,i_0_35,i_0_51,i_0_22,i_0_23,i_0_26,i_0_41]) ).
cnf(i_0_54,plain,
less_equal(zero,X1),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_55,plain,
~ quotient(zQy,zero,zero),
inference(scs_inference,[],[i_0_34,i_0_27,i_0_28,i_0_35,i_0_51,i_0_22,i_0_23,i_0_26,i_0_41,i_0_21]) ).
cnf(i_0_56,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_57,plain,
( ~ quotient(X1,X2,X3)
| X4 = X3
| ~ quotient(X1,X2,X4) ),
inference(rename_variables,[],[i_0_21]) ).
cnf(i_0_58,plain,
identity != zQx,
inference(scs_inference,[],[i_0_34,i_0_27,i_0_28,i_0_35,i_0_51,i_0_36,i_0_22,i_0_23,i_0_26,i_0_41,i_0_21,i_0_42]) ).
cnf(i_0_59,plain,
less_equal(X1,identity),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_60,plain,
zQy != zQx,
inference(scs_inference,[],[i_0_34,i_0_27,i_0_56,i_0_28,i_0_35,i_0_51,i_0_36,i_0_22,i_0_23,i_0_26,i_0_41,i_0_21,i_0_42,i_0_43]) ).
cnf(i_0_61,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_62,plain,
zQy != zero,
inference(scs_inference,[],[i_0_34,i_0_27,i_0_56,i_0_28,i_0_35,i_0_51,i_0_36,i_0_22,i_0_23,i_0_26,i_0_41,i_0_21,i_0_42,i_0_43,i_0_44]) ).
cnf(i_0_63,plain,
quotient(X1,X1,zero),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_64,plain,
zQx != zQy,
inference(scs_inference,[],[i_0_34,i_0_27,i_0_56,i_0_61,i_0_28,i_0_35,i_0_51,i_0_36,i_0_22,i_0_23,i_0_26,i_0_41,i_0_21,i_0_42,i_0_43,i_0_44,i_0_45]) ).
cnf(i_0_65,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_66,plain,
~ less_equal(divide(zQy,zQx),zero),
inference(scs_inference,[],[i_0_34,i_0_27,i_0_56,i_0_61,i_0_65,i_0_28,i_0_24,i_0_35,i_0_51,i_0_36,i_0_22,i_0_23,i_0_26,i_0_41,i_0_21,i_0_42,i_0_43,i_0_44,i_0_45,i_0_20]) ).
cnf(i_0_67,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_68,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_24]) ).
cnf(i_0_69,plain,
( ~ quotient(X1,X2,X3)
| less_equal(X3,X4)
| ~ quotient(X1,X4,X5)
| ~ less_equal(X5,X2) ),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_70,plain,
( ~ less_equal(y,x)
| x = y ),
inference(scs_inference,[],[i_0_34,i_0_27,i_0_56,i_0_61,i_0_65,i_0_28,i_0_24,i_0_35,i_0_51,i_0_36,i_0_37,i_0_22,i_0_23,i_0_26,i_0_41,i_0_21,i_0_42,i_0_43,i_0_44,i_0_45,i_0_20,i_0_33]) ).
cnf(i_0_71,plain,
( ~ less_equal(X1,X2)
| ~ less_equal(X2,X1)
| X1 = X2 ),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_72,plain,
( ~ quotient(zero,zero,zQx)
| ~ quotient(zero,zero,zQy) ),
inference(scs_inference,[],[i_0_34,i_0_27,i_0_56,i_0_61,i_0_65,i_0_67,i_0_28,i_0_24,i_0_68,i_0_35,i_0_51,i_0_36,i_0_37,i_0_22,i_0_23,i_0_26,i_0_41,i_0_21,i_0_42,i_0_43,i_0_44,i_0_45,i_0_20,i_0_33,i_0_19]) ).
cnf(i_0_73,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_24]) ).
cnf(i_0_74,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_75,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_76,plain,
( ~ quotient(X1,X2,X3)
| ~ quotient(X4,X5,X6)
| less_equal(X3,X6)
| ~ quotient(X7,X8,X4)
| ~ quotient(X8,X5,X2)
| ~ quotient(X7,X5,X1) ),
inference(rename_variables,[],[i_0_19]) ).
cnf(i_0_77,plain,
~ quotient(zero,X1,zQy),
inference(scs_inference,[],[i_0_50,i_0_22]) ).
cnf(i_0_78,plain,
( less_equal(X1,X2)
| ~ quotient(X2,X3,X1) ),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_79,plain,
~ quotient(X1,identity,zQy),
inference(scs_inference,[],[i_0_50,i_0_30,i_0_62,i_0_22,i_0_21]) ).
cnf(i_0_80,plain,
( ~ quotient(X1,X2,X3)
| X4 = X3
| ~ quotient(X1,X2,X4) ),
inference(rename_variables,[],[i_0_21]) ).
cnf(i_0_81,plain,
zero != divide(zQy,zQx),
inference(scs_inference,[],[i_0_48,i_0_50,i_0_66,i_0_30,i_0_62,i_0_22,i_0_21,i_0_41]) ).
cnf(i_0_82,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_48]) ).
cnf(i_0_83,plain,
divide(zQy,zQx) != zero,
inference(scs_inference,[],[i_0_48,i_0_82,i_0_50,i_0_66,i_0_30,i_0_62,i_0_22,i_0_21,i_0_41,i_0_42]) ).
cnf(i_0_84,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_48]) ).
cnf(i_0_85,plain,
z != zQx,
inference(scs_inference,[],[i_0_48,i_0_82,i_0_50,i_0_46,i_0_66,i_0_30,i_0_31,i_0_62,i_0_22,i_0_21,i_0_41,i_0_42,i_0_43]) ).
cnf(i_0_86,plain,
~ quotient(zQx,X1,zQy),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_87,plain,
identity != zero,
inference(scs_inference,[],[i_0_48,i_0_82,i_0_50,i_0_46,i_0_66,i_0_30,i_0_31,i_0_55,i_0_62,i_0_22,i_0_21,i_0_41,i_0_42,i_0_43,i_0_44]) ).
cnf(i_0_88,plain,
quotient(X1,identity,zero),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_89,plain,
~ less_equal(divide(z,zQx),y),
inference(scs_inference,[],[i_0_34,i_0_48,i_0_82,i_0_50,i_0_46,i_0_66,i_0_30,i_0_31,i_0_55,i_0_62,i_0_24,i_0_22,i_0_21,i_0_41,i_0_42,i_0_43,i_0_44,i_0_20]) ).
cnf(i_0_90,plain,
quotient(X1,X2,divide(X1,X2)),
inference(rename_variables,[],[i_0_24]) ).
cnf(i_0_91,plain,
( ~ quotient(X1,X2,X3)
| less_equal(X3,X4)
| ~ quotient(X1,X4,X5)
| ~ less_equal(X5,X2) ),
inference(rename_variables,[],[i_0_20]) ).
cnf(i_0_92,plain,
~ less_equal(divide(z,zQx),x),
inference(scs_inference,[],[i_0_34,i_0_48,i_0_82,i_0_50,i_0_46,i_0_66,i_0_30,i_0_31,i_0_55,i_0_62,i_0_24,i_0_37,i_0_22,i_0_21,i_0_41,i_0_42,i_0_43,i_0_44,i_0_20,i_0_26]) ).
cnf(i_0_93,plain,
( ~ less_equal(X1,X2)
| less_equal(X3,X2)
| ~ less_equal(X3,X1) ),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_94,plain,
~ quotient(x,X1,divide(z,zQx)),
inference(scs_inference,[],[i_0_92,i_0_22]) ).
cnf(i_0_95,plain,
( less_equal(X1,X2)
| ~ quotient(X2,X3,X1) ),
inference(rename_variables,[],[i_0_22]) ).
cnf(i_0_96,plain,
~ quotient(zero,X1,divide(zQy,zQx)),
inference(scs_inference,[],[i_0_92,i_0_29,i_0_83,i_0_22,i_0_21]) ).
cnf(i_0_97,plain,
( ~ quotient(X1,X2,X3)
| X4 = X3
| ~ quotient(X1,X2,X4) ),
inference(rename_variables,[],[i_0_21]) ).
cnf(i_0_98,plain,
x != divide(z,zQx),
inference(scs_inference,[],[i_0_92,i_0_29,i_0_83,i_0_27,i_0_22,i_0_21,i_0_45]) ).
cnf(i_0_99,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_100,plain,
divide(z,zQx) != x,
inference(scs_inference,[],[i_0_92,i_0_29,i_0_83,i_0_27,i_0_99,i_0_22,i_0_21,i_0_45,i_0_43]) ).
cnf(i_0_101,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_102,plain,
zero != identity,
inference(scs_inference,[],[i_0_92,i_0_29,i_0_79,i_0_83,i_0_27,i_0_99,i_0_101,i_0_22,i_0_21,i_0_45,i_0_43,i_0_44]) ).
cnf(i_0_103,plain,
~ quotient(X1,identity,zQy),
inference(rename_variables,[],[i_0_79]) ).
cnf(i_0_104,plain,
quotient(X1,zero,X1),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_105,plain,
y != divide(z,zQx),
inference(scs_inference,[],[i_0_92,i_0_89,i_0_48,i_0_29,i_0_79,i_0_83,i_0_27,i_0_99,i_0_101,i_0_22,i_0_21,i_0_45,i_0_43,i_0_44,i_0_41]) ).
cnf(i_0_106,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_48]) ).
cnf(i_0_107,plain,
divide(z,zQx) != y,
inference(scs_inference,[],[i_0_92,i_0_89,i_0_48,i_0_106,i_0_29,i_0_79,i_0_83,i_0_27,i_0_99,i_0_101,i_0_22,i_0_21,i_0_45,i_0_43,i_0_44,i_0_41,i_0_42]) ).
cnf(i_0_108,plain,
less_equal(X1,X1),
inference(rename_variables,[],[i_0_48]) ).
cnf(i_0_109,plain,
$false,
inference(scs_inference,[],[i_0_92,i_0_89,i_0_48,i_0_106,i_0_108,i_0_29,i_0_79,i_0_83,i_0_32,i_0_27,i_0_99,i_0_101,i_0_24,i_0_22,i_0_21,i_0_45,i_0_43,i_0_44,i_0_41,i_0_42,i_0_20]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : HEN007-2 : TPTP v9.2.1. Released v1.0.0.
% 0.11/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.33 % Computer : n006.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Mon May 4 19:09:01 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 0.31/1.62 % Version : CSE_E---1.7
% 0.31/1.62 % Problem : theBenchmark.p
% 0.31/1.62 % SZS status Unsatisfiable for theBenchmark.p
% 0.31/1.62 % SZS output start CNFRefutation
% See solution above
% 0.41/1.79 % Total time : 1.270s
%------------------------------------------------------------------------------