%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYO607+1 : TPTP v9.0.0. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 : Fri Jul 25 09:59:04 PM UTC 2025
% Result : Theorem 34.15s 4.66s
% Output : CNFRefutation 34.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 5
% Syntax : Number of formulae : 81 ( 20 unt; 0 def)
% Number of atoms : 217 ( 0 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 239 ( 103 ~; 112 |; 21 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 2 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-1 aty)
% Number of variables : 62 ( 8 sgn 14 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(nc6,plain,
( ? [A] :
( g_false_only(a,A)
& ? [B] : g_false_only(A,B) )
| ? [A] :
! [B] : g_true_only(A,B)
| ( ? [A] :
( ( g_both(a,A)
| ( ? [B] : g_both(A,B)
& ~ ? [B] : g_false_only(A,B) ) )
& ~ g_true_only(a,A)
& ~ ! [B] : g_true_only(A,B) )
& ~ ? [A] :
( g_false_only(a,A)
& ? [B] : g_false_only(A,B) )
& ? [A] :
( ? [B] : g_both(A,B)
& ~ ? [B] : g_false_only(A,B) )
& ~ ? [A] :
! [B] : g_true_only(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nc6) ).
fof(nc6_negated,plain,
~ ( ? [A] :
( g_false_only(a,A)
& ? [B] : g_false_only(A,B) )
| ? [A] :
! [B] : g_true_only(A,B)
| ( ? [A] :
( ( g_both(a,A)
| ( ? [B] : g_both(A,B)
& ~ ? [B] : g_false_only(A,B) ) )
& ~ g_true_only(a,A)
& ~ ! [B] : g_true_only(A,B) )
& ~ ? [A] :
( g_false_only(a,A)
& ? [B] : g_false_only(A,B) )
& ? [A] :
( ? [B] : g_both(A,B)
& ~ ? [B] : g_false_only(A,B) )
& ~ ? [A] :
! [B] : g_true_only(A,B) ) ),
inference(negate_conjecture,[status(cth)],[nc6]) ).
cnf(2,plain,
( ~ g_both(X0,X1)
| ~ g_both(a,X2)
| sP0
| g_false_only(X0,sK5(X0))
| g_true_only(X2,X3)
| g_true_only(a,X2)
| g_true_only(sK6,X4) ),
inference(cnf,[status(esa)],[nc6_negated]) ).
cnf(l0,plain,
( ~ g_both(a,sK1(a))
| ~ g_both(a,sK1(a))
| sP0
| g_false_only(a,sK5(a))
| g_true_only(sK1(a),sK1(sK1(a)))
| g_true_only(a,sK1(a))
| g_true_only(sK6,sK1(sK6)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(1,plain,
~ g_true_only(X0,sK1(X0)),
inference(cnf,[status(esa)],[nc6_negated]) ).
cnf(l3121,plain,
~ g_true_only(sK1(a),sK1(sK1(a))),
inference(instantiation,[status(thm)],[1]) ).
fof(exhaustion_g,plain,
! [X_2,X_1] :
( g_true_only(X_2,X_1)
| g_both(X_2,X_1)
| g_false_only(X_2,X_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exhaustion_g) ).
cnf(15,plain,
( g_both(X0,X1)
| g_false_only(X0,X1)
| g_true_only(X0,X1) ),
inference(cnf,[status(esa)],[exhaustion_g]) ).
cnf(l1,plain,
( g_both(a,sK1(a))
| g_false_only(a,sK1(a))
| g_true_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3122,plain,
~ g_true_only(a,sK1(a)),
inference(instantiation,[status(thm)],[1]) ).
cnf(5,plain,
( g_false_only(a,sK3)
| ~ sP0 ),
inference(cnf,[status(esa)],[nc6_negated]) ).
cnf(l3100,plain,
( g_false_only(a,sK3)
| ~ sP0 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3,plain,
~ g_true_only(a,sK1(a)),
inference(instantiation,[status(thm)],[1]) ).
fof(both_g,plain,
! [X_2,X_1] :
( g_both(X_2,X_1)
<=> ( g_true(X_2,X_1)
& g_false(X_2,X_1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',both_g) ).
cnf(11,plain,
( ~ g_false(X0,X1)
| ~ g_true(X0,X1)
| g_both(X0,X1) ),
inference(cnf,[status(esa)],[both_g]) ).
cnf(l2,plain,
( ~ g_false(a,sK1(a))
| ~ g_true(a,sK1(a))
| g_both(a,sK1(a)) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(0,plain,
( ~ g_false_only(X0,X1)
| ~ g_false_only(a,X0) ),
inference(cnf,[status(esa)],[nc6_negated]) ).
cnf(l3101,plain,
( ~ g_false_only(sK3,sK4)
| ~ g_false_only(a,sK3) ),
inference(instantiation,[status(thm)],[0]) ).
fof(false_only_g,plain,
! [X_2,X_1] :
( g_false_only(X_2,X_1)
<=> ( g_false(X_2,X_1)
& ~ g_true(X_2,X_1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',false_only_g) ).
cnf(12,plain,
( ~ g_false_only(X0,X1)
| g_false(X0,X1) ),
inference(cnf,[status(esa)],[false_only_g]) ).
cnf(l17,plain,
( ~ g_false_only(a,sK1(a))
| g_false(a,sK1(a)) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3102,plain,
( ~ g_false_only(sK5(a),sK2(sK5(a)))
| ~ g_false_only(a,sK5(a)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(4,plain,
( g_false_only(sK3,sK4)
| ~ sP0 ),
inference(cnf,[status(esa)],[nc6_negated]) ).
cnf(l3103,plain,
( g_false_only(sK3,sK4)
| ~ sP0 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l55,plain,
( g_both(a,sK1(a))
| g_false_only(a,sK1(a))
| g_true_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(3,plain,
( ~ g_both(X0,X1)
| ~ g_both(X2,X3)
| sP0
| g_false_only(X0,sK2(X0))
| g_false_only(X2,sK5(X2))
| g_true_only(X0,X4)
| g_true_only(a,X0)
| g_true_only(sK6,X5) ),
inference(cnf,[status(esa)],[nc6_negated]) ).
cnf(l3537,plain,
( ~ g_both(sK5(a),sK1(sK5(a)))
| ~ g_both(sK5(a),sK1(sK5(a)))
| sP0
| g_false_only(sK5(a),sK2(sK5(a)))
| g_false_only(sK5(a),sK5(sK5(a)))
| g_true_only(sK5(a),sK1(sK5(a)))
| g_true_only(a,sK5(a))
| g_true_only(sK6,sK1(sK6)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l16,plain,
( ~ g_false_only(sK1(a),sK5(sK1(a)))
| ~ g_false_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[0]) ).
fof(true_only_g,plain,
! [X_2,X_1] :
( g_true_only(X_2,X_1)
<=> ( g_true(X_2,X_1)
& ~ g_false(X_2,X_1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',true_only_g) ).
cnf(6,plain,
( ~ g_true_only(X0,X1)
| g_true(X0,X1) ),
inference(cnf,[status(esa)],[true_only_g]) ).
cnf(l9,plain,
( ~ g_true_only(a,sK1(a))
| g_true(a,sK1(a)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l3538,plain,
( ~ g_true_only(a,sK5(a))
| g_true(a,sK5(a)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(13,plain,
( ~ g_false_only(X0,X1)
| ~ g_true(X0,X1) ),
inference(cnf,[status(esa)],[false_only_g]) ).
cnf(l4308,plain,
( ~ g_false_only(a,sK5(a))
| ~ g_true(a,sK5(a)) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l58,plain,
( ~ g_both(sK1(a),sK1(sK1(a)))
| ~ g_both(sK1(a),sK1(sK1(a)))
| sP0
| g_false_only(sK1(a),sK2(sK1(a)))
| g_false_only(sK1(a),sK5(sK1(a)))
| g_true_only(sK1(a),sK1(sK1(a)))
| g_true_only(a,sK1(a))
| g_true_only(sK6,sK1(sK6)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3042,plain,
~ g_true_only(a,sK1(a)),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3539,plain,
~ g_true_only(sK6,sK1(sK6)),
inference(instantiation,[status(thm)],[1]) ).
cnf(l62,plain,
~ g_true_only(a,sK1(a)),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3093,plain,
( ~ g_false_only(sK1(a),sK2(sK1(a)))
| ~ g_false_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3542,plain,
( g_false_only(a,sK3)
| ~ sP0 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l218,plain,
( g_false_only(a,sK3)
| ~ sP0 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3551,plain,
( g_both(sK5(a),sK1(sK5(a)))
| g_false_only(sK5(a),sK1(sK5(a)))
| g_true_only(sK5(a),sK1(sK5(a))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l448,plain,
( ~ g_both(sK1(a),sK1(sK1(a)))
| ~ g_both(sK1(a),sK1(sK1(a)))
| sP0
| g_false_only(sK1(a),sK2(sK1(a)))
| g_false_only(sK1(a),sK5(sK1(a)))
| g_true_only(sK1(a),sK1(sK1(a)))
| g_true_only(a,sK1(a))
| g_true_only(sK6,sK1(sK6)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3429,plain,
( ~ g_false_only(sK1(a),sK2(sK1(a)))
| ~ g_false_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3511,plain,
~ g_true_only(sK6,sK1(sK6)),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3123,plain,
~ g_true_only(sK6,sK1(sK6)),
inference(instantiation,[status(thm)],[1]) ).
cnf(l469,plain,
( g_false_only(sK3,sK4)
| ~ sP0 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3837,plain,
~ g_true_only(sK1(a),sK1(sK1(a))),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3544,plain,
( g_both(sK5(a),sK1(sK5(a)))
| g_false_only(sK5(a),sK1(sK5(a)))
| g_true_only(sK5(a),sK1(sK5(a))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3559,plain,
( ~ g_false_only(sK3,sK4)
| ~ g_false_only(a,sK3) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3509,plain,
( ~ g_false_only(sK3,sK4)
| ~ g_false_only(a,sK3) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3540,plain,
~ g_true_only(sK5(a),sK1(sK5(a))),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3043,plain,
~ g_true_only(sK1(a),sK1(sK1(a))),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3418,plain,
( ~ g_false_only(sK1(a),sK5(sK1(a)))
| ~ g_false_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1825,plain,
( g_both(sK1(a),sK1(sK1(a)))
| g_false_only(sK1(a),sK1(sK1(a)))
| g_true_only(sK1(a),sK1(sK1(a))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l459,plain,
( g_both(sK1(a),sK1(sK1(a)))
| g_false_only(sK1(a),sK1(sK1(a)))
| g_true_only(sK1(a),sK1(sK1(a))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3553,plain,
~ g_true_only(sK5(a),sK1(sK5(a))),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3580,plain,
( g_false_only(a,sK3)
| ~ sP0 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3606,plain,
~ g_true_only(sK1(a),sK1(sK1(a))),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3045,plain,
~ g_true_only(sK1(a),sK1(sK1(a))),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3591,plain,
( g_both(a,sK1(a))
| g_false_only(a,sK1(a))
| g_true_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3573,plain,
( g_both(a,sK1(a))
| g_false_only(a,sK1(a))
| g_true_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4379,plain,
( g_false_only(sK3,sK4)
| ~ sP0 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3664,plain,
~ g_true_only(sK5(a),sK1(sK5(a))),
inference(instantiation,[status(thm)],[1]) ).
cnf(l471,plain,
( ~ g_false_only(sK1(a),sK1(sK1(a)))
| ~ g_false_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l485,plain,
( g_both(sK1(a),sK1(sK1(a)))
| g_false_only(sK1(a),sK1(sK1(a)))
| g_true_only(sK1(a),sK1(sK1(a))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3554,plain,
( ~ g_false_only(sK5(a),sK1(sK5(a)))
| ~ g_false_only(a,sK5(a)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3583,plain,
( ~ g_false_only(sK5(a),sK1(sK5(a)))
| ~ g_false_only(a,sK5(a)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3041,plain,
( ~ g_false_only(sK3,sK4)
| ~ g_false_only(a,sK3) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l474,plain,
( g_both(a,sK1(a))
| g_false_only(a,sK1(a))
| g_true_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1664,plain,
( ~ g_false_only(sK1(a),sK1(sK1(a)))
| ~ g_false_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1679,plain,
( g_both(a,sK1(a))
| g_false_only(a,sK1(a))
| g_true_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3044,plain,
~ g_true_only(sK6,sK1(sK6)),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3547,plain,
( ~ g_false_only(sK5(a),sK5(sK5(a)))
| ~ g_false_only(a,sK5(a)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1828,plain,
( ~ g_false_only(sK1(a),sK1(sK1(a)))
| ~ g_false_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l60,plain,
( g_both(sK1(a),sK1(sK1(a)))
| g_false_only(sK1(a),sK1(sK1(a)))
| g_true_only(sK1(a),sK1(sK1(a))) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l76,plain,
~ g_true_only(sK1(a),sK1(sK1(a))),
inference(instantiation,[status(thm)],[1]) ).
cnf(l325,plain,
( ~ g_false_only(sK1(a),sK1(sK1(a)))
| ~ g_false_only(a,sK1(a)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3051,plain,
( g_false_only(sK3,sK4)
| ~ sP0 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1382,plain,
~ g_true_only(sK1(a),sK1(sK1(a))),
inference(instantiation,[status(thm)],[1]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l3121,l1,l3122,l3100,l3,l2,l3101,l17,l3102,l3103,l55,l3537,l16,l9,l3538,l4308,l58,l3042,l3539,l62,l3093,l3542,l218,l3551,l448,l3429,l3511,l3123,l469,l3837,l3544,l3559,l3509,l3540,l3043,l3418,l1825,l459,l3553,l3580,l3606,l3045,l3591,l3573,l4379,l3664,l471,l485,l3554,l3583,l3041,l474,l1664,l1679,l3044,l3547,l1828,l60,l76,l325,l3051,l1382]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.12 % Problem : SYO607+1 : TPTP v9.0.0. Released v7.0.0.
% 0.02/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n018.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Tue Jul 22 19:55:49 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % launching worker at depth: 1
% 0.13/0.34 % launching worker at depth: 5
% 0.13/0.34 % launching worker at depth: 3
% 0.13/0.34 % launching worker at depth: 4
% 0.13/0.34 % launching worker at depth: 6
% 0.13/0.34 % launching worker at depth: 7
% 0.13/0.34 % launching worker at depth: 2
% 0.13/0.34 % launching worker at depth: 8
% 0.13/0.34 % launching worker at depth: 9
% 0.13/0.35 % launching worker at depth: 10
% 0.20/0.36 % launching worker at depth: 11
% 0.20/0.52 % launching worker at depth: 12
% 6.01/1.15 % launching worker at depth: 13
% 34.15/4.66 % SZS status Theorem for theBenchmark
% 34.15/4.66 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------