%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : LCL664+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 : Mon Sep 7 12:14:14 PM UTC 2026
% Result : Theorem 6.69s 1.24s
% Output : CNFRefutation 6.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 1
% Syntax : Number of formulae : 158 ( 92 unt; 0 def)
% Number of atoms : 1111 ( 0 equ)
% Maximal formula atoms : 390 ( 7 avg)
% Number of connectives : 2031 (1078 ~; 825 |; 128 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 81 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 32 ( 31 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-4 aty)
% Number of variables : 535 ( 0 sgn 508 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(main,plain,
~ ? [X] :
~ ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| p56(Y) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| p54(Y) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| p54(Y) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| p52(Y) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p56(Y) )
& ~ p46(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p56(Y) )
& ~ p44(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p56(Y) )
& ~ p42(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p54(Y) )
& ~ p46(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p54(Y) )
& ~ p44(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p54(Y) )
& ~ p42(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p52(Y) )
& ~ p46(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p52(Y) )
& ~ p44(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p52(Y) )
& ~ p42(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p46(X) )
& ~ p36(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p46(X) )
& ~ p32(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p55(Y) )
& ~ p45(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p53(Y) )
& ~ p45(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p51(Y) )
& ~ p45(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p44(X) )
& ~ p36(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p44(X) )
& ~ p32(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p55(Y) )
& ~ p43(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p53(Y) )
& ~ p43(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p51(Y) )
& ~ p43(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p42(X) )
& ~ p36(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p42(X) )
& ~ p32(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p55(Y) )
& ~ p41(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p54(Y) )
& ~ p41(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p53(Y) )
& ~ p41(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p51(Y) )
& ~ p41(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p36(Y) )
& ~ p26(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p36(Y) )
& ~ p24(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p36(Y) )
& ~ p22(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p45(X) )
& ~ p35(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p43(X) )
& ~ p35(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p34(Y) )
& ~ p26(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p34(Y) )
& ~ p24(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p34(Y) )
& ~ p22(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p41(X) )
& ~ p34(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p45(X) )
& ~ p33(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p43(X) )
& ~ p33(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p32(Y) )
& ~ p26(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p32(Y) )
& ~ p24(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p32(Y) )
& ~ p22(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p45(X) )
& ~ p31(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p43(X) )
& ~ p31(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p26(X) )
& ~ p16(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p26(X) )
& ~ p14(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p35(Y) )
& ~ p25(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p33(Y) )
& ~ p25(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p31(Y) )
& ~ p25(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p24(X) )
& ~ p16(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p24(X) )
& ~ p14(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p35(Y) )
& ~ p23(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p33(Y) )
& ~ p23(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p31(Y) )
& ~ p23(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p22(X) )
& ~ p16(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p22(X) )
& ~ p14(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p35(Y) )
& ~ p21(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p34(Y) )
& ~ p21(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p33(Y) )
& ~ p21(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p31(Y) )
& ~ p21(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p25(X) )
& ~ p15(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p23(X) )
& ~ p15(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p25(X) )
& ~ p13(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p23(X) )
& ~ p13(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p21(X) )
& ~ p12(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p25(X) )
& ~ p11(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p23(X) )
& ~ p11(Y) ) )
| ! [Y] :
( ~ r1(X,Y)
| p15(Y) )
| ! [Y] :
( ~ r1(X,Y)
| p13(Y) )
| ! [Y] :
( ~ r1(X,Y)
| p12(Y) )
| ! [Y] :
( ~ r1(X,Y)
| p11(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(main_negated,plain,
~ ~ ? [X] :
~ ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| p56(Y) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| p54(Y) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| p54(Y) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| p52(Y) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p56(Y) )
& ~ p46(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p56(Y) )
& ~ p44(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p56(Y) )
& ~ p42(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p54(Y) )
& ~ p46(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p54(Y) )
& ~ p44(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p54(Y) )
& ~ p42(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p52(Y) )
& ~ p46(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p52(Y) )
& ~ p44(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p52(Y) )
& ~ p42(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p46(X) )
& ~ p36(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p46(X) )
& ~ p32(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p55(Y) )
& ~ p45(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p53(Y) )
& ~ p45(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p51(Y) )
& ~ p45(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p44(X) )
& ~ p36(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p44(X) )
& ~ p32(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p55(Y) )
& ~ p43(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p53(Y) )
& ~ p43(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p51(Y) )
& ~ p43(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p42(X) )
& ~ p36(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p42(X) )
& ~ p32(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p55(Y) )
& ~ p41(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p54(Y) )
& ~ p41(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p53(Y) )
& ~ p41(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p51(Y) )
& ~ p41(X) ) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p36(Y) )
& ~ p26(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p36(Y) )
& ~ p24(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p36(Y) )
& ~ p22(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p45(X) )
& ~ p35(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p43(X) )
& ~ p35(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p34(Y) )
& ~ p26(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p34(Y) )
& ~ p24(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p34(Y) )
& ~ p22(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p41(X) )
& ~ p34(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p45(X) )
& ~ p33(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p43(X) )
& ~ p33(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p32(Y) )
& ~ p26(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p32(Y) )
& ~ p24(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p32(Y) )
& ~ p22(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p45(X) )
& ~ p31(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p43(X) )
& ~ p31(Y) ) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p26(X) )
& ~ p16(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p26(X) )
& ~ p14(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p35(Y) )
& ~ p25(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p33(Y) )
& ~ p25(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p31(Y) )
& ~ p25(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p24(X) )
& ~ p16(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p24(X) )
& ~ p14(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p35(Y) )
& ~ p23(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p33(Y) )
& ~ p23(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p31(Y) )
& ~ p23(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p22(X) )
& ~ p16(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p22(X) )
& ~ p14(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p35(Y) )
& ~ p21(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p34(Y) )
& ~ p21(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p33(Y) )
& ~ p21(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ! [Y] :
( ~ r1(X,Y)
| p31(Y) )
& ~ p21(X) ) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p25(X) )
& ~ p15(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p23(X) )
& ~ p15(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p25(X) )
& ~ p13(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p23(X) )
& ~ p13(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p21(X) )
& ~ p12(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p25(X) )
& ~ p11(Y) ) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ! [X] :
( ~ r1(Y,X)
| p23(X) )
& ~ p11(Y) ) )
| ! [Y] :
( ~ r1(X,Y)
| p15(Y) )
| ! [Y] :
( ~ r1(X,Y)
| p13(Y) )
| ! [Y] :
( ~ r1(X,Y)
| p12(Y) )
| ! [Y] :
( ~ r1(X,Y)
| p11(Y) ) ),
inference(negate_conjecture,[status(cth)],[main]) ).
cnf(2,plain,
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(sK1,X0)
| p54(X4) ),
inference(cnf,[status(esa)],[main_negated]) ).
cnf(l0,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK63(sK68),sK56(sK68,sK63(sK68)))
| ~ r1(sK56(sK68,sK63(sK68)),sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68))))
| ~ r1(sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68))),sK24(sK68,sK63(sK68),sK56(sK68,sK63(sK68)),sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68)))))
| ~ r1(sK1,sK68)
| p54(sK24(sK68,sK63(sK68),sK56(sK68,sK63(sK68)),sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68))))) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(50,plain,
( ~ p54(sK24(X0,X1,X2,X3))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(sK1,X0)
| p41(X3) ),
inference(cnf,[status(esa)],[main_negated]) ).
cnf(l4,plain,
( ~ p54(sK24(sK68,sK63(sK68),sK56(sK68,sK63(sK68)),sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68)))))
| ~ r1(sK68,sK63(sK68))
| ~ r1(sK63(sK68),sK56(sK68,sK63(sK68)))
| ~ r1(sK56(sK68,sK63(sK68)),sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68))))
| ~ r1(sK1,sK68)
| p41(sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68)))) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(72,plain,
( ~ p41(sK35(X0,X1,X2))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(sK1,X0)
| p34(X2) ),
inference(cnf,[status(esa)],[main_negated]) ).
cnf(l9,plain,
( ~ p41(sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68))))
| ~ r1(sK68,sK63(sK68))
| ~ r1(sK63(sK68),sK56(sK68,sK63(sK68)))
| ~ r1(sK1,sK68)
| p34(sK56(sK68,sK63(sK68))) ),
inference(instantiation,[status(thm)],[72]) ).
cnf(71,plain,
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(sK1,X0)
| p34(X2)
| r1(X2,sK35(X0,X1,X2)) ),
inference(cnf,[status(esa)],[main_negated]) ).
cnf(l10,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK63(sK68),sK56(sK68,sK63(sK68)))
| ~ r1(sK1,sK68)
| p34(sK56(sK68,sK63(sK68)))
| r1(sK56(sK68,sK63(sK68)),sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68)))) ),
inference(instantiation,[status(thm)],[71]) ).
cnf(114,plain,
( ~ p34(sK56(X0,X1))
| ~ r1(X0,X1)
| ~ r1(sK1,X0)
| p21(X1) ),
inference(cnf,[status(esa)],[main_negated]) ).
cnf(l346,plain,
( ~ p34(sK56(sK68,sK63(sK68)))
| ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68)) ),
inference(instantiation,[status(thm)],[114]) ).
cnf(l28,plain,
( ~ p34(sK56(sK68,sK63(sK68)))
| ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68)) ),
inference(instantiation,[status(thm)],[114]) ).
cnf(49,plain,
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(sK1,X0)
| p41(X3)
| r1(X3,sK24(X0,X1,X2,X3)) ),
inference(cnf,[status(esa)],[main_negated]) ).
cnf(l31,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK63(sK68),sK56(sK68,sK63(sK68)))
| ~ r1(sK56(sK68,sK63(sK68)),sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68))))
| ~ r1(sK1,sK68)
| p41(sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68))))
| r1(sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68))),sK24(sK68,sK63(sK68),sK56(sK68,sK63(sK68)),sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68))))) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(137,plain,
r1(sK1,sK68),
inference(cnf,[status(esa)],[main_negated]) ).
cnf(l213,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(128,plain,
( ~ p21(sK63(X0))
| ~ r1(sK1,X0)
| p12(X0) ),
inference(cnf,[status(esa)],[main_negated]) ).
cnf(l611,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(127,plain,
( ~ r1(sK1,X0)
| p12(X0)
| r1(X0,sK63(X0)) ),
inference(cnf,[status(esa)],[main_negated]) ).
cnf(l214,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(113,plain,
( ~ r1(X0,X1)
| ~ r1(sK1,X0)
| p21(X1)
| r1(X1,sK56(X0,X1)) ),
inference(cnf,[status(esa)],[main_negated]) ).
cnf(l37,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68))
| r1(sK63(sK68),sK56(sK68,sK63(sK68))) ),
inference(instantiation,[status(thm)],[113]) ).
cnf(l1,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK63(sK68),sK56(sK68,sK63(sK68)))
| ~ r1(sK1,sK68)
| p34(sK56(sK68,sK63(sK68)))
| r1(sK56(sK68,sK63(sK68)),sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68)))) ),
inference(instantiation,[status(thm)],[71]) ).
cnf(l11,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l99,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68))
| r1(sK63(sK68),sK56(sK68,sK63(sK68))) ),
inference(instantiation,[status(thm)],[113]) ).
cnf(l205,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l13,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l656,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(138,plain,
~ p12(sK68),
inference(cnf,[status(esa)],[main_negated]) ).
cnf(l1135,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l344,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68))
| r1(sK63(sK68),sK56(sK68,sK63(sK68))) ),
inference(instantiation,[status(thm)],[113]) ).
cnf(l260,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l967,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l18,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68))
| r1(sK63(sK68),sK56(sK68,sK63(sK68))) ),
inference(instantiation,[status(thm)],[113]) ).
cnf(l50,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK63(sK68),sK56(sK68,sK63(sK68)))
| ~ r1(sK1,sK68)
| p34(sK56(sK68,sK63(sK68)))
| r1(sK56(sK68,sK63(sK68)),sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68)))) ),
inference(instantiation,[status(thm)],[71]) ).
cnf(l89,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l76,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l374,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l415,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l27,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68))
| r1(sK63(sK68),sK56(sK68,sK63(sK68))) ),
inference(instantiation,[status(thm)],[113]) ).
cnf(l143,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l428,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l411,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l87,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l119,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l420,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l66,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l140,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l106,plain,
( ~ p41(sK35(sK68,sK63(sK68),sK56(sK68,sK63(sK68))))
| ~ r1(sK68,sK63(sK68))
| ~ r1(sK63(sK68),sK56(sK68,sK63(sK68)))
| ~ r1(sK1,sK68)
| p34(sK56(sK68,sK63(sK68))) ),
inference(instantiation,[status(thm)],[72]) ).
cnf(l488,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l791,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l457,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l138,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l240,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l490,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l541,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1103,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l222,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l204,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l537,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68))
| r1(sK63(sK68),sK56(sK68,sK63(sK68))) ),
inference(instantiation,[status(thm)],[113]) ).
cnf(l63,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l482,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1057,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l107,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l105,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l852,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l805,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l139,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l96,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l496,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l434,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68))
| r1(sK63(sK68),sK56(sK68,sK63(sK68))) ),
inference(instantiation,[status(thm)],[113]) ).
cnf(l960,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l968,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l1104,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l426,plain,
( ~ p34(sK56(sK68,sK63(sK68)))
| ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68)) ),
inference(instantiation,[status(thm)],[114]) ).
cnf(l94,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l435,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l469,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l3,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l499,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l357,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l849,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l492,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l879,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l388,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l489,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l1056,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l196,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1079,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l1173,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1107,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1171,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l1076,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l880,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l532,plain,
( ~ p34(sK56(sK68,sK63(sK68)))
| ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68)) ),
inference(instantiation,[status(thm)],[114]) ).
cnf(l1136,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l857,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1169,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l250,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l2,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l868,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l470,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l1170,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l1109,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l1168,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l1174,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l6,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l1066,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l43,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l19,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l803,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l126,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l497,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l548,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l1164,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l462,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l1005,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l20,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l853,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l80,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l875,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l1165,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l88,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l801,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l957,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1073,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l15,plain,
( ~ p34(sK56(sK68,sK63(sK68)))
| ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68)) ),
inference(instantiation,[status(thm)],[114]) ).
cnf(l647,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l876,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l97,plain,
( ~ r1(sK68,sK63(sK68))
| ~ r1(sK1,sK68)
| p21(sK63(sK68))
| r1(sK63(sK68),sK56(sK68,sK63(sK68))) ),
inference(instantiation,[status(thm)],[113]) ).
cnf(l98,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1053,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l101,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l533,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l137,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l132,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l316,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l267,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1172,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l26,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1067,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1167,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l116,plain,
( ~ p21(sK63(sK68))
| ~ r1(sK1,sK68)
| p12(sK68) ),
inference(instantiation,[status(thm)],[128]) ).
cnf(l74,plain,
( ~ r1(sK1,sK68)
| p12(sK68)
| r1(sK68,sK63(sK68)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l191,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1068,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l759,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l927,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1175,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l332,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l463,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l340,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(l129,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l1166,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l758,plain,
r1(sK1,sK68),
inference(instantiation,[status(thm)],[137]) ).
cnf(l928,plain,
~ p12(sK68),
inference(instantiation,[status(thm)],[138]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l4,l9,l10,l346,l28,l31,l213,l611,l214,l37,l1,l11,l99,l205,l13,l656,l1135,l344,l260,l967,l18,l50,l89,l76,l374,l415,l27,l143,l428,l411,l87,l119,l420,l66,l140,l106,l488,l791,l457,l138,l240,l490,l541,l1103,l222,l204,l537,l63,l482,l1057,l107,l105,l852,l805,l139,l96,l496,l434,l960,l968,l1104,l426,l94,l435,l469,l3,l499,l357,l849,l492,l879,l388,l489,l1056,l196,l1079,l1173,l1107,l1171,l1076,l880,l532,l1136,l857,l1169,l250,l2,l868,l470,l1170,l1109,l1168,l1174,l6,l1066,l43,l19,l803,l126,l497,l548,l1164,l462,l1005,l20,l853,l80,l875,l1165,l88,l801,l957,l1073,l15,l647,l876,l97,l98,l1053,l101,l533,l137,l132,l316,l267,l1172,l26,l1067,l1167,l116,l74,l191,l1068,l759,l927,l1175,l332,l463,l340,l129,l1166,l758,l928]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL664+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n003.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 5 01:41:20 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % launching worker at depth: 1
% 0.08/0.36 % launching worker at depth: 8
% 0.08/0.36 % launching worker at depth: 4
% 0.08/0.36 % launching worker at depth: 2
% 0.08/0.36 % launching worker at depth: 5
% 0.08/0.36 % launching worker at depth: 6
% 0.08/0.36 % launching worker at depth: 7
% 0.08/0.36 % launching worker at depth: 3
% 0.13/0.42 % launching worker at depth: 9
% 4.31/0.97 % launching worker at depth: 10
% 6.69/1.24 % SZS status Theorem for theBenchmark
% 6.69/1.24 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------