%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : PUZ075+1 : TPTP v9.0.0. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n031.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 01:24:36 PM UTC 2025
% Result : Theorem 0.19s 0.45s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 3
% Syntax : Number of formulae : 11 ( 5 unt; 0 def)
% Number of atoms : 379 ( 364 equ)
% Maximal formula atoms : 361 ( 34 avg)
% Number of connectives : 377 ( 9 ~; 186 |; 180 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 184 ( 19 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 100 ( 100 usr; 100 con; 0-0 aty)
% Number of variables : 8 ( 0 sgn 4 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tlhfof24989,plain,
adj(cell12,cell13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tlhfof24989) ).
fof(tlhfof24989_negated,plain,
~ adj(cell12,cell13),
inference(negate_conjecture,[status(cth)],[tlhfof24989]) ).
cnf(543,plain,
~ adj(cell12,cell13),
inference(cnf,[status(esa)],[tlhfof24989_negated]) ).
cnf(l0,plain,
~ adj(cell12,cell13),
inference(instantiation,[status(thm)],[543]) ).
fof(tlhfof24988,plain,
! [Y,X] :
( adj(X,Y)
<=> ( edge(X,Y)
| edge(Y,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tlhfof24988) ).
cnf(541,plain,
( ~ edge(X0,X1)
| adj(X0,X1) ),
inference(cnf,[status(esa)],[tlhfof24988]) ).
cnf(l1,plain,
( ~ edge(cell12,cell13)
| adj(cell12,cell13) ),
inference(instantiation,[status(thm)],[541]) ).
fof(tlhfof24987,plain,
! [TLH24985,TLH24986] :
( edge(TLH24986,TLH24985)
<=> ( ( TLH24986 = cell1
& TLH24985 = cell2 )
| ( TLH24986 = cell2
& TLH24985 = cell3 )
| ( TLH24986 = cell3
& TLH24985 = cell4 )
| ( TLH24986 = cell4
& TLH24985 = cell5 )
| ( TLH24986 = cell5
& TLH24985 = cell6 )
| ( TLH24986 = cell6
& TLH24985 = cell7 )
| ( TLH24986 = cell7
& TLH24985 = cell8 )
| ( TLH24986 = cell8
& TLH24985 = cell9 )
| ( TLH24986 = cell9
& TLH24985 = cell10 )
| ( TLH24986 = cell11
& TLH24985 = cell12 )
| ( TLH24986 = cell12
& TLH24985 = cell13 )
| ( TLH24986 = cell13
& TLH24985 = cell14 )
| ( TLH24986 = cell14
& TLH24985 = cell15 )
| ( TLH24986 = cell15
& TLH24985 = cell16 )
| ( TLH24986 = cell16
& TLH24985 = cell17 )
| ( TLH24986 = cell17
& TLH24985 = cell18 )
| ( TLH24986 = cell18
& TLH24985 = cell19 )
| ( TLH24986 = cell19
& TLH24985 = cell20 )
| ( TLH24986 = cell21
& TLH24985 = cell22 )
| ( TLH24986 = cell22
& TLH24985 = cell23 )
| ( TLH24986 = cell23
& TLH24985 = cell24 )
| ( TLH24986 = cell24
& TLH24985 = cell25 )
| ( TLH24986 = cell25
& TLH24985 = cell26 )
| ( TLH24986 = cell26
& TLH24985 = cell27 )
| ( TLH24986 = cell27
& TLH24985 = cell28 )
| ( TLH24986 = cell28
& TLH24985 = cell29 )
| ( TLH24986 = cell29
& TLH24985 = cell30 )
| ( TLH24986 = cell31
& TLH24985 = cell32 )
| ( TLH24986 = cell32
& TLH24985 = cell33 )
| ( TLH24986 = cell33
& TLH24985 = cell34 )
| ( TLH24986 = cell34
& TLH24985 = cell35 )
| ( TLH24986 = cell35
& TLH24985 = cell36 )
| ( TLH24986 = cell36
& TLH24985 = cell37 )
| ( TLH24986 = cell37
& TLH24985 = cell38 )
| ( TLH24986 = cell38
& TLH24985 = cell39 )
| ( TLH24986 = cell39
& TLH24985 = cell40 )
| ( TLH24986 = cell41
& TLH24985 = cell42 )
| ( TLH24986 = cell42
& TLH24985 = cell43 )
| ( TLH24986 = cell43
& TLH24985 = cell44 )
| ( TLH24986 = cell44
& TLH24985 = cell45 )
| ( TLH24986 = cell45
& TLH24985 = cell46 )
| ( TLH24986 = cell46
& TLH24985 = cell47 )
| ( TLH24986 = cell47
& TLH24985 = cell48 )
| ( TLH24986 = cell48
& TLH24985 = cell49 )
| ( TLH24986 = cell49
& TLH24985 = cell50 )
| ( TLH24986 = cell51
& TLH24985 = cell52 )
| ( TLH24986 = cell52
& TLH24985 = cell53 )
| ( TLH24986 = cell53
& TLH24985 = cell54 )
| ( TLH24986 = cell54
& TLH24985 = cell55 )
| ( TLH24986 = cell55
& TLH24985 = cell56 )
| ( TLH24986 = cell56
& TLH24985 = cell57 )
| ( TLH24986 = cell57
& TLH24985 = cell58 )
| ( TLH24986 = cell58
& TLH24985 = cell59 )
| ( TLH24986 = cell59
& TLH24985 = cell60 )
| ( TLH24986 = cell61
& TLH24985 = cell62 )
| ( TLH24986 = cell62
& TLH24985 = cell63 )
| ( TLH24986 = cell63
& TLH24985 = cell64 )
| ( TLH24986 = cell64
& TLH24985 = cell65 )
| ( TLH24986 = cell65
& TLH24985 = cell66 )
| ( TLH24986 = cell66
& TLH24985 = cell67 )
| ( TLH24986 = cell67
& TLH24985 = cell68 )
| ( TLH24986 = cell68
& TLH24985 = cell69 )
| ( TLH24986 = cell69
& TLH24985 = cell70 )
| ( TLH24986 = cell71
& TLH24985 = cell72 )
| ( TLH24986 = cell72
& TLH24985 = cell73 )
| ( TLH24986 = cell73
& TLH24985 = cell74 )
| ( TLH24986 = cell74
& TLH24985 = cell75 )
| ( TLH24986 = cell75
& TLH24985 = cell76 )
| ( TLH24986 = cell76
& TLH24985 = cell77 )
| ( TLH24986 = cell77
& TLH24985 = cell78 )
| ( TLH24986 = cell78
& TLH24985 = cell79 )
| ( TLH24986 = cell79
& TLH24985 = cell80 )
| ( TLH24986 = cell81
& TLH24985 = cell82 )
| ( TLH24986 = cell82
& TLH24985 = cell83 )
| ( TLH24986 = cell83
& TLH24985 = cell84 )
| ( TLH24986 = cell84
& TLH24985 = cell85 )
| ( TLH24986 = cell85
& TLH24985 = cell86 )
| ( TLH24986 = cell86
& TLH24985 = cell87 )
| ( TLH24986 = cell87
& TLH24985 = cell88 )
| ( TLH24986 = cell88
& TLH24985 = cell89 )
| ( TLH24986 = cell89
& TLH24985 = cell90 )
| ( TLH24986 = cell91
& TLH24985 = cell92 )
| ( TLH24986 = cell92
& TLH24985 = cell93 )
| ( TLH24986 = cell93
& TLH24985 = cell94 )
| ( TLH24986 = cell94
& TLH24985 = cell95 )
| ( TLH24986 = cell95
& TLH24985 = cell96 )
| ( TLH24986 = cell96
& TLH24985 = cell97 )
| ( TLH24986 = cell97
& TLH24985 = cell98 )
| ( TLH24986 = cell98
& TLH24985 = cell99 )
| ( TLH24986 = cell99
& TLH24985 = cell100 )
| ( TLH24986 = cell1
& TLH24985 = cell11 )
| ( TLH24986 = cell2
& TLH24985 = cell12 )
| ( TLH24986 = cell3
& TLH24985 = cell13 )
| ( TLH24986 = cell4
& TLH24985 = cell14 )
| ( TLH24986 = cell5
& TLH24985 = cell15 )
| ( TLH24986 = cell6
& TLH24985 = cell16 )
| ( TLH24986 = cell7
& TLH24985 = cell17 )
| ( TLH24986 = cell8
& TLH24985 = cell18 )
| ( TLH24986 = cell9
& TLH24985 = cell19 )
| ( TLH24986 = cell10
& TLH24985 = cell20 )
| ( TLH24986 = cell11
& TLH24985 = cell21 )
| ( TLH24986 = cell12
& TLH24985 = cell22 )
| ( TLH24986 = cell13
& TLH24985 = cell23 )
| ( TLH24986 = cell14
& TLH24985 = cell24 )
| ( TLH24986 = cell15
& TLH24985 = cell25 )
| ( TLH24986 = cell16
& TLH24985 = cell26 )
| ( TLH24986 = cell17
& TLH24985 = cell27 )
| ( TLH24986 = cell18
& TLH24985 = cell28 )
| ( TLH24986 = cell19
& TLH24985 = cell29 )
| ( TLH24986 = cell20
& TLH24985 = cell30 )
| ( TLH24986 = cell21
& TLH24985 = cell31 )
| ( TLH24986 = cell22
& TLH24985 = cell32 )
| ( TLH24986 = cell23
& TLH24985 = cell33 )
| ( TLH24986 = cell24
& TLH24985 = cell34 )
| ( TLH24986 = cell25
& TLH24985 = cell35 )
| ( TLH24986 = cell26
& TLH24985 = cell36 )
| ( TLH24986 = cell27
& TLH24985 = cell37 )
| ( TLH24986 = cell28
& TLH24985 = cell38 )
| ( TLH24986 = cell29
& TLH24985 = cell39 )
| ( TLH24986 = cell30
& TLH24985 = cell40 )
| ( TLH24986 = cell31
& TLH24985 = cell41 )
| ( TLH24986 = cell32
& TLH24985 = cell42 )
| ( TLH24986 = cell33
& TLH24985 = cell43 )
| ( TLH24986 = cell34
& TLH24985 = cell44 )
| ( TLH24986 = cell35
& TLH24985 = cell45 )
| ( TLH24986 = cell36
& TLH24985 = cell46 )
| ( TLH24986 = cell37
& TLH24985 = cell47 )
| ( TLH24986 = cell38
& TLH24985 = cell48 )
| ( TLH24986 = cell39
& TLH24985 = cell49 )
| ( TLH24986 = cell40
& TLH24985 = cell50 )
| ( TLH24986 = cell41
& TLH24985 = cell51 )
| ( TLH24986 = cell42
& TLH24985 = cell52 )
| ( TLH24986 = cell43
& TLH24985 = cell53 )
| ( TLH24986 = cell44
& TLH24985 = cell54 )
| ( TLH24986 = cell45
& TLH24985 = cell55 )
| ( TLH24986 = cell46
& TLH24985 = cell56 )
| ( TLH24986 = cell47
& TLH24985 = cell57 )
| ( TLH24986 = cell48
& TLH24985 = cell58 )
| ( TLH24986 = cell49
& TLH24985 = cell59 )
| ( TLH24986 = cell50
& TLH24985 = cell60 )
| ( TLH24986 = cell51
& TLH24985 = cell61 )
| ( TLH24986 = cell52
& TLH24985 = cell62 )
| ( TLH24986 = cell53
& TLH24985 = cell63 )
| ( TLH24986 = cell54
& TLH24985 = cell64 )
| ( TLH24986 = cell55
& TLH24985 = cell65 )
| ( TLH24986 = cell56
& TLH24985 = cell66 )
| ( TLH24986 = cell57
& TLH24985 = cell67 )
| ( TLH24986 = cell58
& TLH24985 = cell68 )
| ( TLH24986 = cell59
& TLH24985 = cell69 )
| ( TLH24986 = cell60
& TLH24985 = cell70 )
| ( TLH24986 = cell61
& TLH24985 = cell71 )
| ( TLH24986 = cell62
& TLH24985 = cell72 )
| ( TLH24986 = cell63
& TLH24985 = cell73 )
| ( TLH24986 = cell64
& TLH24985 = cell74 )
| ( TLH24986 = cell65
& TLH24985 = cell75 )
| ( TLH24986 = cell66
& TLH24985 = cell76 )
| ( TLH24986 = cell67
& TLH24985 = cell77 )
| ( TLH24986 = cell68
& TLH24985 = cell78 )
| ( TLH24986 = cell69
& TLH24985 = cell79 )
| ( TLH24986 = cell70
& TLH24985 = cell80 )
| ( TLH24986 = cell71
& TLH24985 = cell81 )
| ( TLH24986 = cell72
& TLH24985 = cell82 )
| ( TLH24986 = cell73
& TLH24985 = cell83 )
| ( TLH24986 = cell74
& TLH24985 = cell84 )
| ( TLH24986 = cell75
& TLH24985 = cell85 )
| ( TLH24986 = cell76
& TLH24985 = cell86 )
| ( TLH24986 = cell77
& TLH24985 = cell87 )
| ( TLH24986 = cell78
& TLH24985 = cell88 )
| ( TLH24986 = cell79
& TLH24985 = cell89 )
| ( TLH24986 = cell80
& TLH24985 = cell90 )
| ( TLH24986 = cell81
& TLH24985 = cell91 )
| ( TLH24986 = cell82
& TLH24985 = cell92 )
| ( TLH24986 = cell83
& TLH24985 = cell93 )
| ( TLH24986 = cell84
& TLH24985 = cell94 )
| ( TLH24986 = cell85
& TLH24985 = cell95 )
| ( TLH24986 = cell86
& TLH24985 = cell96 )
| ( TLH24986 = cell87
& TLH24985 = cell97 )
| ( TLH24986 = cell88
& TLH24985 = cell98 )
| ( TLH24986 = cell89
& TLH24985 = cell99 )
| ( TLH24986 = cell90
& TLH24985 = cell100 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tlhfof24987) ).
cnf(12,plain,
( X0 != cell13
| X1 != cell12
| edge(X1,X0) ),
inference(cnf,[status(esa)],[tlhfof24987]) ).
cnf(l2,plain,
( cell13 != cell13
| cell12 != cell12
| edge(cell12,cell13) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : PUZ075+1 : TPTP v9.0.0. Released v3.5.0.
% 0.11/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n031.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Jul 21 16:09:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.35 % launching worker at depth: 1
% 0.12/0.35 % launching worker at depth: 4
% 0.12/0.35 % launching worker at depth: 3
% 0.12/0.35 % launching worker at depth: 2
% 0.12/0.35 % launching worker at depth: 6
% 0.12/0.35 % launching worker at depth: 7
% 0.12/0.35 % launching worker at depth: 8
% 0.12/0.35 % launching worker at depth: 5
% 0.12/0.35 % launching worker at depth: 9
% 0.12/0.36 % launching worker at depth: 10
% 0.19/0.45 % SZS status Theorem for theBenchmark
% 0.19/0.45 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------