%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SYO691-1.001 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n014.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 : 600s
% DateTime : Thu Jul 21 18:40:56 EDT 2022
% Result : Unsatisfiable 1.07s 1.25s
% Output : CNFRefutation 1.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 7
% Syntax : Number of clauses : 43 ( 22 unt; 0 nHn; 20 RR)
% Number of literals : 69 ( 0 equ; 28 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 165 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(rule_1,axiom,
top(f(f(f(Z,a),Y),f(X,a)),f(f(X,f(f(Y,a),a)),Z)) ).
cnf(prove,negated_conjecture,
~ seq(succ(succ(succ(succ(succ(zero))))),X,X) ).
cnf(rewrite_top,axiom,
( ~ top(X,Y)
| step(X,Y) ) ).
cnf(rewrite_left,axiom,
( ~ step(X,Y)
| step(f(X,Z),f(Y,Z)) ) ).
cnf(rewrite_right,axiom,
( ~ step(Y,Z)
| step(f(X,Y),f(X,Z)) ) ).
cnf(rewrite_sequence_zero,axiom,
seq(zero,X,X) ).
cnf(rewrite_sequence_succ,axiom,
( ~ seq(N,X,Y)
| ~ step(Y,Z)
| seq(succ(N),X,Z) ) ).
cnf(refute_0_0,plain,
~ seq(succ(succ(succ(succ(succ(zero))))),f(f(f(f(f(a,a),a),f(f(f(f(f(f(a,a),a),a),a),a),a)),f(a,a)),f(f(f(f(a,a),a),f(f(f(f(a,a),a),a),a)),a)),f(f(f(f(f(a,a),a),f(f(f(f(f(f(a,a),a),a),a),a),a)),f(a,a)),f(f(f(f(a,a),a),f(f(f(f(a,a),a),a),a)),a))),
inference(subst,[],[prove:[bind(X,$fot(f(f(f(f(f(a,a),a),f(f(f(f(f(f(a,a),a),a),a),a),a)),f(a,a)),f(f(f(f(a,a),a),f(f(f(f(a,a),a),a),a)),a))))]]) ).
cnf(refute_0_1,plain,
( ~ top(f(f(f(X_6,a),X_5),f(X_4,a)),f(f(X_4,f(f(X_5,a),a)),X_6))
| step(f(f(f(X_6,a),X_5),f(X_4,a)),f(f(X_4,f(f(X_5,a),a)),X_6)) ),
inference(subst,[],[rewrite_top:[bind(X,$fot(f(f(f(X_6,a),X_5),f(X_4,a)))),bind(Y,$fot(f(f(X_4,f(f(X_5,a),a)),X_6)))]]) ).
cnf(refute_0_2,plain,
top(f(f(f(X_6,a),X_5),f(X_4,a)),f(f(X_4,f(f(X_5,a),a)),X_6)),
inference(subst,[],[rule_1:[bind(X,$fot(X_4)),bind(Y,$fot(X_5)),bind(Z,$fot(X_6))]]) ).
cnf(refute_0_3,plain,
step(f(f(f(X_6,a),X_5),f(X_4,a)),f(f(X_4,f(f(X_5,a),a)),X_6)),
inference(resolve,[$cnf( top(f(f(f(X_6,a),X_5),f(X_4,a)),f(f(X_4,f(f(X_5,a),a)),X_6)) )],[refute_0_2,refute_0_1]) ).
cnf(refute_0_4,plain,
( ~ step(f(f(f(X_6,a),X_5),f(X_4,a)),f(f(X_4,f(f(X_5,a),a)),X_6))
| step(f(f(f(f(X_6,a),X_5),f(X_4,a)),X_12),f(f(f(X_4,f(f(X_5,a),a)),X_6),X_12)) ),
inference(subst,[],[rewrite_left:[bind(X,$fot(f(f(f(X_6,a),X_5),f(X_4,a)))),bind(Y,$fot(f(f(X_4,f(f(X_5,a),a)),X_6))),bind(Z,$fot(X_12))]]) ).
cnf(refute_0_5,plain,
step(f(f(f(f(X_6,a),X_5),f(X_4,a)),X_12),f(f(f(X_4,f(f(X_5,a),a)),X_6),X_12)),
inference(resolve,[$cnf( step(f(f(f(X_6,a),X_5),f(X_4,a)),f(f(X_4,f(f(X_5,a),a)),X_6)) )],[refute_0_3,refute_0_4]) ).
cnf(refute_0_6,plain,
( ~ seq(X_39,X_40,f(f(f(f(X_6,a),X_5),f(X_4,a)),X_12))
| ~ step(f(f(f(f(X_6,a),X_5),f(X_4,a)),X_12),f(f(f(X_4,f(f(X_5,a),a)),X_6),X_12))
| seq(succ(X_39),X_40,f(f(f(X_4,f(f(X_5,a),a)),X_6),X_12)) ),
inference(subst,[],[rewrite_sequence_succ:[bind(N,$fot(X_39)),bind(X,$fot(X_40)),bind(Y,$fot(f(f(f(f(X_6,a),X_5),f(X_4,a)),X_12))),bind(Z,$fot(f(f(f(X_4,f(f(X_5,a),a)),X_6),X_12)))]]) ).
cnf(refute_0_7,plain,
( ~ seq(X_39,X_40,f(f(f(f(X_6,a),X_5),f(X_4,a)),X_12))
| seq(succ(X_39),X_40,f(f(f(X_4,f(f(X_5,a),a)),X_6),X_12)) ),
inference(resolve,[$cnf( step(f(f(f(f(X_6,a),X_5),f(X_4,a)),X_12),f(f(f(X_4,f(f(X_5,a),a)),X_6),X_12)) )],[refute_0_5,refute_0_6]) ).
cnf(refute_0_8,plain,
( ~ seq(succ(succ(succ(succ(zero)))),f(f(f(f(f(a,a),X_1505),f(f(f(f(X_1504,a),a),X_1508),a)),X_1507),f(f(f(X_6,a),X_5),a)),f(f(f(f(X_6,a),X_5),f(f(X_1507,a),a)),f(f(X_1504,f(f(f(f(X_1508,a),a),a),a)),X_1505)))
| seq(succ(succ(succ(succ(succ(zero))))),f(f(f(f(f(a,a),X_1505),f(f(f(f(X_1504,a),a),X_1508),a)),X_1507),f(f(f(X_6,a),X_5),a)),f(f(f(f(X_1507,a),f(f(X_5,a),a)),X_6),f(f(X_1504,f(f(f(f(X_1508,a),a),a),a)),X_1505))) ),
inference(subst,[],[refute_0_7:[bind(X_12,$fot(f(f(X_1504,f(f(f(f(X_1508,a),a),a),a)),X_1505))),bind(X_39,$fot(succ(succ(succ(succ(zero)))))),bind(X_4,$fot(f(X_1507,a))),bind(X_40,$fot(f(f(f(f(f(a,a),X_1505),f(f(f(f(X_1504,a),a),X_1508),a)),X_1507),f(f(f(X_6,a),X_5),a))))]]) ).
cnf(refute_0_9,plain,
( ~ step(f(f(f(X_6,a),X_5),f(X_4,a)),f(f(X_4,f(f(X_5,a),a)),X_6))
| step(f(X_13,f(f(f(X_6,a),X_5),f(X_4,a))),f(X_13,f(f(X_4,f(f(X_5,a),a)),X_6))) ),
inference(subst,[],[rewrite_right:[bind(X,$fot(X_13)),bind(Y,$fot(f(f(f(X_6,a),X_5),f(X_4,a)))),bind(Z,$fot(f(f(X_4,f(f(X_5,a),a)),X_6)))]]) ).
cnf(refute_0_10,plain,
step(f(X_13,f(f(f(X_6,a),X_5),f(X_4,a))),f(X_13,f(f(X_4,f(f(X_5,a),a)),X_6))),
inference(resolve,[$cnf( step(f(f(f(X_6,a),X_5),f(X_4,a)),f(f(X_4,f(f(X_5,a),a)),X_6)) )],[refute_0_3,refute_0_9]) ).
cnf(refute_0_11,plain,
( ~ seq(X_39,X_40,f(X_13,f(f(f(X_6,a),X_5),f(X_4,a))))
| ~ step(f(X_13,f(f(f(X_6,a),X_5),f(X_4,a))),f(X_13,f(f(X_4,f(f(X_5,a),a)),X_6)))
| seq(succ(X_39),X_40,f(X_13,f(f(X_4,f(f(X_5,a),a)),X_6))) ),
inference(subst,[],[rewrite_sequence_succ:[bind(N,$fot(X_39)),bind(X,$fot(X_40)),bind(Y,$fot(f(X_13,f(f(f(X_6,a),X_5),f(X_4,a))))),bind(Z,$fot(f(X_13,f(f(X_4,f(f(X_5,a),a)),X_6))))]]) ).
cnf(refute_0_12,plain,
( ~ seq(X_39,X_40,f(X_13,f(f(f(X_6,a),X_5),f(X_4,a))))
| seq(succ(X_39),X_40,f(X_13,f(f(X_4,f(f(X_5,a),a)),X_6))) ),
inference(resolve,[$cnf( step(f(X_13,f(f(f(X_6,a),X_5),f(X_4,a))),f(X_13,f(f(X_4,f(f(X_5,a),a)),X_6))) )],[refute_0_10,refute_0_11]) ).
cnf(refute_0_13,plain,
( ~ seq(succ(succ(succ(zero))),f(f(f(f(f(a,a),X_476),f(f(f(f(X_4,a),a),X_479),a)),X_478),f(X_477,a)),f(f(X_477,f(f(X_478,a),a)),f(f(f(X_476,a),f(f(X_479,a),a)),f(X_4,a))))
| seq(succ(succ(succ(succ(zero)))),f(f(f(f(f(a,a),X_476),f(f(f(f(X_4,a),a),X_479),a)),X_478),f(X_477,a)),f(f(X_477,f(f(X_478,a),a)),f(f(X_4,f(f(f(f(X_479,a),a),a),a)),X_476))) ),
inference(subst,[],[refute_0_12:[bind(X_13,$fot(f(X_477,f(f(X_478,a),a)))),bind(X_39,$fot(succ(succ(succ(zero))))),bind(X_40,$fot(f(f(f(f(f(a,a),X_476),f(f(f(f(X_4,a),a),X_479),a)),X_478),f(X_477,a)))),bind(X_5,$fot(f(f(X_479,a),a))),bind(X_6,$fot(X_476))]]) ).
cnf(refute_0_14,plain,
( ~ step(f(f(f(f(X_23,a),X_22),f(X_21,a)),X_20),f(f(f(X_21,f(f(X_22,a),a)),X_23),X_20))
| step(f(f(f(f(f(X_23,a),X_22),f(X_21,a)),X_20),Z),f(f(f(f(X_21,f(f(X_22,a),a)),X_23),X_20),Z)) ),
inference(subst,[],[rewrite_left:[bind(X,$fot(f(f(f(f(X_23,a),X_22),f(X_21,a)),X_20))),bind(Y,$fot(f(f(f(X_21,f(f(X_22,a),a)),X_23),X_20)))]]) ).
cnf(refute_0_15,plain,
step(f(f(f(f(X_23,a),X_22),f(X_21,a)),X_20),f(f(f(X_21,f(f(X_22,a),a)),X_23),X_20)),
inference(subst,[],[refute_0_5:[bind(X_12,$fot(X_20)),bind(X_4,$fot(X_21)),bind(X_5,$fot(X_22)),bind(X_6,$fot(X_23))]]) ).
cnf(refute_0_16,plain,
step(f(f(f(f(f(X_23,a),X_22),f(X_21,a)),X_20),Z),f(f(f(f(X_21,f(f(X_22,a),a)),X_23),X_20),Z)),
inference(resolve,[$cnf( step(f(f(f(f(X_23,a),X_22),f(X_21,a)),X_20),f(f(f(X_21,f(f(X_22,a),a)),X_23),X_20)) )],[refute_0_15,refute_0_14]) ).
cnf(refute_0_17,plain,
seq(zero,X_41,X_41),
inference(subst,[],[rewrite_sequence_zero:[bind(X,$fot(X_41))]]) ).
cnf(refute_0_18,plain,
( ~ seq(zero,X_41,X_41)
| ~ step(X_41,X_42)
| seq(succ(zero),X_41,X_42) ),
inference(subst,[],[rewrite_sequence_succ:[bind(N,$fot(zero)),bind(X,$fot(X_41)),bind(Y,$fot(X_41)),bind(Z,$fot(X_42))]]) ).
cnf(refute_0_19,plain,
( ~ step(X_41,X_42)
| seq(succ(zero),X_41,X_42) ),
inference(resolve,[$cnf( seq(zero,X_41,X_41) )],[refute_0_17,refute_0_18]) ).
cnf(refute_0_20,plain,
( ~ step(f(f(f(f(f(X_23,a),X_22),f(X_21,a)),X_20),Z),f(f(f(f(X_21,f(f(X_22,a),a)),X_23),X_20),Z))
| seq(succ(zero),f(f(f(f(f(X_23,a),X_22),f(X_21,a)),X_20),Z),f(f(f(f(X_21,f(f(X_22,a),a)),X_23),X_20),Z)) ),
inference(subst,[],[refute_0_19:[bind(X_41,$fot(f(f(f(f(f(X_23,a),X_22),f(X_21,a)),X_20),Z))),bind(X_42,$fot(f(f(f(f(X_21,f(f(X_22,a),a)),X_23),X_20),Z)))]]) ).
cnf(refute_0_21,plain,
seq(succ(zero),f(f(f(f(f(X_23,a),X_22),f(X_21,a)),X_20),Z),f(f(f(f(X_21,f(f(X_22,a),a)),X_23),X_20),Z)),
inference(resolve,[$cnf( step(f(f(f(f(f(X_23,a),X_22),f(X_21,a)),X_20),Z),f(f(f(f(X_21,f(f(X_22,a),a)),X_23),X_20),Z)) )],[refute_0_16,refute_0_20]) ).
cnf(refute_0_22,plain,
seq(succ(zero),f(f(f(f(f(a,a),X_22),f(X_21,a)),X_239),f(X_237,a)),f(f(f(f(X_21,f(f(X_22,a),a)),a),X_239),f(X_237,a))),
inference(subst,[],[refute_0_21:[bind(Z,$fot(f(X_237,a))),bind(X_20,$fot(X_239)),bind(X_23,$fot(a))]]) ).
cnf(refute_0_23,plain,
( ~ seq(X_39,X_40,f(f(f(X_6,a),X_5),f(X_4,a)))
| ~ step(f(f(f(X_6,a),X_5),f(X_4,a)),f(f(X_4,f(f(X_5,a),a)),X_6))
| seq(succ(X_39),X_40,f(f(X_4,f(f(X_5,a),a)),X_6)) ),
inference(subst,[],[rewrite_sequence_succ:[bind(N,$fot(X_39)),bind(X,$fot(X_40)),bind(Y,$fot(f(f(f(X_6,a),X_5),f(X_4,a)))),bind(Z,$fot(f(f(X_4,f(f(X_5,a),a)),X_6)))]]) ).
cnf(refute_0_24,plain,
( ~ seq(X_39,X_40,f(f(f(X_6,a),X_5),f(X_4,a)))
| seq(succ(X_39),X_40,f(f(X_4,f(f(X_5,a),a)),X_6)) ),
inference(resolve,[$cnf( step(f(f(f(X_6,a),X_5),f(X_4,a)),f(f(X_4,f(f(X_5,a),a)),X_6)) )],[refute_0_3,refute_0_23]) ).
cnf(refute_0_25,plain,
( ~ seq(succ(zero),f(f(f(f(f(a,a),X_22),f(X_21,a)),X_239),f(X_237,a)),f(f(f(f(X_21,f(f(X_22,a),a)),a),X_239),f(X_237,a)))
| seq(succ(succ(zero)),f(f(f(f(f(a,a),X_22),f(X_21,a)),X_239),f(X_237,a)),f(f(X_237,f(f(X_239,a),a)),f(X_21,f(f(X_22,a),a)))) ),
inference(subst,[],[refute_0_24:[bind(X_39,$fot(succ(zero))),bind(X_4,$fot(X_237)),bind(X_40,$fot(f(f(f(f(f(a,a),X_22),f(X_21,a)),X_239),f(X_237,a)))),bind(X_5,$fot(X_239)),bind(X_6,$fot(f(X_21,f(f(X_22,a),a))))]]) ).
cnf(refute_0_26,plain,
seq(succ(succ(zero)),f(f(f(f(f(a,a),X_22),f(X_21,a)),X_239),f(X_237,a)),f(f(X_237,f(f(X_239,a),a)),f(X_21,f(f(X_22,a),a)))),
inference(resolve,[$cnf( seq(succ(zero),f(f(f(f(f(a,a),X_22),f(X_21,a)),X_239),f(X_237,a)),f(f(f(f(X_21,f(f(X_22,a),a)),a),X_239),f(X_237,a))) )],[refute_0_22,refute_0_25]) ).
cnf(refute_0_27,plain,
seq(succ(succ(zero)),f(f(f(f(f(a,a),X_22),f(f(f(X_469,a),X_468),a)),X_239),f(X_237,a)),f(f(X_237,f(f(X_239,a),a)),f(f(f(X_469,a),X_468),f(f(X_22,a),a)))),
inference(subst,[],[refute_0_26:[bind(X_21,$fot(f(f(X_469,a),X_468)))]]) ).
cnf(refute_0_28,plain,
( ~ seq(succ(succ(zero)),f(f(f(f(f(a,a),X_22),f(f(f(X_469,a),X_468),a)),X_239),f(X_237,a)),f(f(X_237,f(f(X_239,a),a)),f(f(f(X_469,a),X_468),f(f(X_22,a),a))))
| seq(succ(succ(succ(zero))),f(f(f(f(f(a,a),X_22),f(f(f(X_469,a),X_468),a)),X_239),f(X_237,a)),f(f(X_237,f(f(X_239,a),a)),f(f(f(X_22,a),f(f(X_468,a),a)),X_469))) ),
inference(subst,[],[refute_0_12:[bind(X_13,$fot(f(X_237,f(f(X_239,a),a)))),bind(X_39,$fot(succ(succ(zero)))),bind(X_4,$fot(f(X_22,a))),bind(X_40,$fot(f(f(f(f(f(a,a),X_22),f(f(f(X_469,a),X_468),a)),X_239),f(X_237,a)))),bind(X_5,$fot(X_468)),bind(X_6,$fot(X_469))]]) ).
cnf(refute_0_29,plain,
seq(succ(succ(succ(zero))),f(f(f(f(f(a,a),X_22),f(f(f(X_469,a),X_468),a)),X_239),f(X_237,a)),f(f(X_237,f(f(X_239,a),a)),f(f(f(X_22,a),f(f(X_468,a),a)),X_469))),
inference(resolve,[$cnf( seq(succ(succ(zero)),f(f(f(f(f(a,a),X_22),f(f(f(X_469,a),X_468),a)),X_239),f(X_237,a)),f(f(X_237,f(f(X_239,a),a)),f(f(f(X_469,a),X_468),f(f(X_22,a),a)))) )],[refute_0_27,refute_0_28]) ).
cnf(refute_0_30,plain,
seq(succ(succ(succ(zero))),f(f(f(f(f(a,a),X_476),f(f(f(f(X_4,a),a),X_479),a)),X_478),f(X_477,a)),f(f(X_477,f(f(X_478,a),a)),f(f(f(X_476,a),f(f(X_479,a),a)),f(X_4,a)))),
inference(subst,[],[refute_0_29:[bind(X_22,$fot(X_476)),bind(X_237,$fot(X_477)),bind(X_239,$fot(X_478)),bind(X_468,$fot(X_479)),bind(X_469,$fot(f(X_4,a)))]]) ).
cnf(refute_0_31,plain,
seq(succ(succ(succ(succ(zero)))),f(f(f(f(f(a,a),X_476),f(f(f(f(X_4,a),a),X_479),a)),X_478),f(X_477,a)),f(f(X_477,f(f(X_478,a),a)),f(f(X_4,f(f(f(f(X_479,a),a),a),a)),X_476))),
inference(resolve,[$cnf( seq(succ(succ(succ(zero))),f(f(f(f(f(a,a),X_476),f(f(f(f(X_4,a),a),X_479),a)),X_478),f(X_477,a)),f(f(X_477,f(f(X_478,a),a)),f(f(f(X_476,a),f(f(X_479,a),a)),f(X_4,a)))) )],[refute_0_30,refute_0_13]) ).
cnf(refute_0_32,plain,
seq(succ(succ(succ(succ(zero)))),f(f(f(f(f(a,a),X_1505),f(f(f(f(X_1504,a),a),X_1508),a)),X_1507),f(f(f(X_6,a),X_5),a)),f(f(f(f(X_6,a),X_5),f(f(X_1507,a),a)),f(f(X_1504,f(f(f(f(X_1508,a),a),a),a)),X_1505))),
inference(subst,[],[refute_0_31:[bind(X_4,$fot(X_1504)),bind(X_476,$fot(X_1505)),bind(X_477,$fot(f(f(X_6,a),X_5))),bind(X_478,$fot(X_1507)),bind(X_479,$fot(X_1508))]]) ).
cnf(refute_0_33,plain,
seq(succ(succ(succ(succ(succ(zero))))),f(f(f(f(f(a,a),X_1505),f(f(f(f(X_1504,a),a),X_1508),a)),X_1507),f(f(f(X_6,a),X_5),a)),f(f(f(f(X_1507,a),f(f(X_5,a),a)),X_6),f(f(X_1504,f(f(f(f(X_1508,a),a),a),a)),X_1505))),
inference(resolve,[$cnf( seq(succ(succ(succ(succ(zero)))),f(f(f(f(f(a,a),X_1505),f(f(f(f(X_1504,a),a),X_1508),a)),X_1507),f(f(f(X_6,a),X_5),a)),f(f(f(f(X_6,a),X_5),f(f(X_1507,a),a)),f(f(X_1504,f(f(f(f(X_1508,a),a),a),a)),X_1505))) )],[refute_0_32,refute_0_8]) ).
cnf(refute_0_34,plain,
seq(succ(succ(succ(succ(succ(zero))))),f(f(f(f(f(a,a),a),f(f(f(f(f(f(a,a),a),a),a),a),a)),f(a,a)),f(f(f(f(a,a),a),f(f(f(f(a,a),a),a),a)),a)),f(f(f(f(f(a,a),a),f(f(f(f(f(f(a,a),a),a),a),a),a)),f(a,a)),f(f(f(f(a,a),a),f(f(f(f(a,a),a),a),a)),a))),
inference(subst,[],[refute_0_33:[bind(X_1504,$fot(f(f(a,a),a))),bind(X_1505,$fot(a)),bind(X_1507,$fot(f(a,a))),bind(X_1508,$fot(a)),bind(X_5,$fot(f(f(f(f(a,a),a),a),a))),bind(X_6,$fot(f(a,a)))]]) ).
cnf(refute_0_35,plain,
$false,
inference(resolve,[$cnf( seq(succ(succ(succ(succ(succ(zero))))),f(f(f(f(f(a,a),a),f(f(f(f(f(f(a,a),a),a),a),a),a)),f(a,a)),f(f(f(f(a,a),a),f(f(f(f(a,a),a),a),a)),a)),f(f(f(f(f(a,a),a),f(f(f(f(f(f(a,a),a),a),a),a),a)),f(a,a)),f(f(f(f(a,a),a),f(f(f(f(a,a),a),a),a)),a))) )],[refute_0_34,refute_0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SYO691-1.001 : TPTP v8.1.0. Released v7.3.0.
% 0.07/0.12 % Command : metis --show proof --show saturation %s
% 0.11/0.33 % Computer : n014.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Sat Jul 9 13:21:50 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.11/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 1.07/1.25 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.07/1.25
% 1.07/1.25 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 1.07/1.26
%------------------------------------------------------------------------------