%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL650+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n012.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:43:05 PM UTC 2026
% Result : Theorem 1.05s 1.35s
% Output : CNFRefutation 1.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 1
% Syntax : Number of formulae : 238 ( 53 unt; 0 def)
% Number of atoms : 1866 ( 0 equ)
% Maximal formula atoms : 46 ( 7 avg)
% Number of connectives : 2976 (1348 ~;1068 |; 520 &)
% ( 0 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 20 con; 0-1 aty)
% Number of variables : 735 ( 0 sgn 408 !; 173 ?)
% Comments :
%------------------------------------------------------------------------------
fof(main,conjecture,
~ ? [X] :
~ ( ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ~ p8(X)
& ~ p6(X)
& ~ p4(X)
& ~ p2(X) ) ) ) ) )
| ! [Y] :
( ~ r1(X,Y)
| p5(Y) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ~ ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p3(X)
& ~ p1(X) )
| ( p1(X)
& p3(X) ) ) ) ) )
| ! [X] :
( ~ r1(Y,X)
| p4(X) )
| ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p2(X)
& ~ p3(X) )
| ( p3(X)
& p2(X) ) ) ) )
| ! [Y] :
( ~ r1(X,Y)
| p3(Y) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p1(X)
& ~ p2(X) )
| ( p2(X)
& p1(X) ) ) ) ) ) ) ) )
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( p4(X)
& p3(X)
& p2(X)
& p1(X) ) ) ) ) ) ) ).
fof(subgoal_0,plain,
! [X] :
( ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ~ p8(X)
& ~ p6(X)
& ~ p4(X)
& ~ p2(X) ) ) ) ) )
& ~ ! [Y] :
( ~ r1(X,Y)
| p5(Y) )
& ~ ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ~ ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p3(X)
& ~ p1(X) )
| ( p1(X)
& p3(X) ) ) ) ) )
| ! [X] :
( ~ r1(Y,X)
| p4(X) )
| ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p2(X)
& ~ p3(X) )
| ( p3(X)
& p2(X) ) ) ) )
| ! [Y] :
( ~ r1(X,Y)
| p3(Y) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p1(X)
& ~ p2(X) )
| ( p2(X)
& p1(X) ) ) ) ) ) ) ) ) )
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ~ ~ r1(Y,X)
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ~ ~ r1(Y,X)
=> p4(X) ) ) ) ) ),
inference(strip,[],[main]) ).
fof(subgoal_1,plain,
! [X] :
( ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ~ p8(X)
& ~ p6(X)
& ~ p4(X)
& ~ p2(X) ) ) ) ) )
& ~ ! [Y] :
( ~ r1(X,Y)
| p5(Y) )
& ~ ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ~ ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p3(X)
& ~ p1(X) )
| ( p1(X)
& p3(X) ) ) ) ) )
| ! [X] :
( ~ r1(Y,X)
| p4(X) )
| ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p2(X)
& ~ p3(X) )
| ( p3(X)
& p2(X) ) ) ) )
| ! [Y] :
( ~ r1(X,Y)
| p3(Y) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p1(X)
& ~ p2(X) )
| ( p2(X)
& p1(X) ) ) ) ) ) ) ) ) )
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ~ ~ r1(Y,X)
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ( ~ ~ r1(Y,X)
& p4(X) )
=> p3(X) ) ) ) ) ),
inference(strip,[],[main]) ).
fof(subgoal_2,plain,
! [X] :
( ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ~ p8(X)
& ~ p6(X)
& ~ p4(X)
& ~ p2(X) ) ) ) ) )
& ~ ! [Y] :
( ~ r1(X,Y)
| p5(Y) )
& ~ ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ~ ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p3(X)
& ~ p1(X) )
| ( p1(X)
& p3(X) ) ) ) ) )
| ! [X] :
( ~ r1(Y,X)
| p4(X) )
| ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p2(X)
& ~ p3(X) )
| ( p3(X)
& p2(X) ) ) ) )
| ! [Y] :
( ~ r1(X,Y)
| p3(Y) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p1(X)
& ~ p2(X) )
| ( p2(X)
& p1(X) ) ) ) ) ) ) ) ) )
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ~ ~ r1(Y,X)
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ( ~ ~ r1(Y,X)
& p4(X)
& p3(X) )
=> p2(X) ) ) ) ) ),
inference(strip,[],[main]) ).
fof(subgoal_3,plain,
! [X] :
( ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ~ p8(X)
& ~ p6(X)
& ~ p4(X)
& ~ p2(X) ) ) ) ) )
& ~ ! [Y] :
( ~ r1(X,Y)
| p5(Y) )
& ~ ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ~ ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p3(X)
& ~ p1(X) )
| ( p1(X)
& p3(X) ) ) ) ) )
| ! [X] :
( ~ r1(Y,X)
| p4(X) )
| ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p2(X)
& ~ p3(X) )
| ( p3(X)
& p2(X) ) ) ) )
| ! [Y] :
( ~ r1(X,Y)
| p3(Y) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p1(X)
& ~ p2(X) )
| ( p2(X)
& p1(X) ) ) ) ) ) ) ) ) )
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ~ ~ r1(Y,X)
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ( ~ ~ r1(Y,X)
& p4(X)
& p3(X)
& p2(X) )
=> p1(X) ) ) ) ) ),
inference(strip,[],[main]) ).
fof(negate_0_0,plain,
~ ! [X] :
( ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ~ p8(X)
& ~ p6(X)
& ~ p4(X)
& ~ p2(X) ) ) ) ) )
& ~ ! [Y] :
( ~ r1(X,Y)
| p5(Y) )
& ~ ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ~ ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p3(X)
& ~ p1(X) )
| ( p1(X)
& p3(X) ) ) ) ) )
| ! [X] :
( ~ r1(Y,X)
| p4(X) )
| ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p2(X)
& ~ p3(X) )
| ( p3(X)
& p2(X) ) ) ) )
| ! [Y] :
( ~ r1(X,Y)
| p3(Y) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p1(X)
& ~ p2(X) )
| ( p2(X)
& p1(X) ) ) ) ) ) ) ) ) )
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ~ ~ r1(Y,X)
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ~ ~ r1(Y,X)
=> p4(X) ) ) ) ) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
? [X] :
( ? [Y] :
( ~ p5(Y)
& r1(X,Y) )
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p4(X)
& r1(Y,X) ) ) ) )
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
( ? [Y] :
( ~ p5(Y)
& r1(skolemFOFtoCNF_X,Y) )
& ? [Y] :
( r1(skolemFOFtoCNF_X,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p4(X)
& r1(Y,X) ) ) ) )
& ? [Y] :
( r1(skolemFOFtoCNF_X,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ) )
& ! [Y] :
( ~ r1(skolemFOFtoCNF_X,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ) ),
inference(skolemize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
? [Y] :
( r1(skolemFOFtoCNF_X,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p4(X)
& r1(Y,X) ) ) ) ),
inference(conjunct,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
( r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
& ? [X] :
( r1(skolemFOFtoCNF_Y_1,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p4(X)
& r1(Y,X) ) ) ) ),
inference(skolemize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
? [X] :
( r1(skolemFOFtoCNF_Y_1,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p4(X)
& r1(Y,X) ) ) ),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_5,plain,
( r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1)
& ? [Y] :
( r1(skolemFOFtoCNF_X_1,Y)
& ? [X] :
( ~ p4(X)
& r1(Y,X) ) ) ),
inference(skolemize,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
? [Y] :
( r1(skolemFOFtoCNF_X_1,Y)
& ? [X] :
( ~ p4(X)
& r1(Y,X) ) ),
inference(conjunct,[],[normalize_0_5]) ).
fof(normalize_0_7,plain,
( r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2)
& ? [X] :
( ~ p4(X)
& r1(skolemFOFtoCNF_Y_2,X) ) ),
inference(skolemize,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
? [X] :
( ~ p4(X)
& r1(skolemFOFtoCNF_Y_2,X) ),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
( ~ p4(skolemFOFtoCNF_X_2)
& r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2) ),
inference(skolemize,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2),
inference(conjunct,[],[normalize_0_9]) ).
fof(normalize_0_11,plain,
r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1),
inference(conjunct,[],[normalize_0_5]) ).
fof(normalize_0_12,plain,
! [Y] :
( ~ r1(skolemFOFtoCNF_X,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ),
inference(conjunct,[],[normalize_0_1]) ).
fof(normalize_0_13,plain,
! [Y] :
( ~ r1(skolemFOFtoCNF_X,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ),
inference(specialize,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
! [X,X0,Y,Y0] :
( ( ~ p4(skolemFOFtoCNF_X_5(Y))
| ~ r1(skolemFOFtoCNF_X,Y) )
& ( ~ r1(skolemFOFtoCNF_X,Y)
| r1(Y,skolemFOFtoCNF_X_5(Y)) )
& ( ~ p3(skolemFOFtoCNF_Y_5(X))
| ~ r1(Y,X)
| ~ r1(skolemFOFtoCNF_X,Y) )
& ( ~ r1(Y,X)
| ~ r1(skolemFOFtoCNF_X,Y)
| r1(X,skolemFOFtoCNF_Y_5(X)) )
& ( ~ p1(X0)
| ~ p2(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y) )
& ( ~ p1(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y) )
& ( ~ p2(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y)
| p1(X0)
| p2(X0) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y)
| p1(X0)
| p3(X0) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y)
| p2(X0)
| p3(X0) ) ),
inference(clausify,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
! [X,X0,Y,Y0] :
( ~ p1(X0)
| ~ p2(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y) ),
inference(conjunct,[],[normalize_0_14]) ).
fof(normalize_0_16,plain,
r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1),
inference(conjunct,[],[normalize_0_3]) ).
fof(normalize_0_17,plain,
r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_18,plain,
! [X,X0,Y,Y0] :
( ~ p1(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y) ),
inference(conjunct,[],[normalize_0_14]) ).
fof(normalize_0_19,plain,
! [X,X0,Y,Y0] :
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y)
| p2(X0)
| p3(X0) ),
inference(conjunct,[],[normalize_0_14]) ).
fof(normalize_0_20,plain,
! [X,X0,Y,Y0] :
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y)
| p1(X0)
| p2(X0) ),
inference(conjunct,[],[normalize_0_14]) ).
fof(normalize_0_21,plain,
! [X,X0,Y,Y0] :
( ~ p2(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y) ),
inference(conjunct,[],[normalize_0_14]) ).
fof(normalize_0_22,plain,
! [X,X0,Y,Y0] :
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y)
| p1(X0)
| p3(X0) ),
inference(conjunct,[],[normalize_0_14]) ).
cnf(refute_0_0,plain,
r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2),
inference(canonicalize,[],[normalize_0_10]) ).
cnf(refute_0_1,plain,
r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1),
inference(canonicalize,[],[normalize_0_11]) ).
cnf(refute_0_2,plain,
( ~ p1(X0)
| ~ p2(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y) ),
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_3,plain,
( ~ p1(X_97)
| ~ p2(X_97)
| ~ r1(X_99,X_97)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_99)
| ~ r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1) ),
inference(subst,[],[refute_0_2:[bind(X,$fot(skolemFOFtoCNF_X_1)),bind(X0,$fot(X_97)),bind(Y,$fot(skolemFOFtoCNF_Y_1)),bind(Y0,$fot(X_99))]]) ).
cnf(refute_0_4,plain,
( ~ p1(X_97)
| ~ p2(X_97)
| ~ r1(X_99,X_97)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_99) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1) )],[refute_0_1,refute_0_3]) ).
cnf(refute_0_5,plain,
r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_6,plain,
( ~ p1(X_97)
| ~ p2(X_97)
| ~ r1(X_99,X_97)
| ~ r1(skolemFOFtoCNF_X_1,X_99) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1) )],[refute_0_5,refute_0_4]) ).
cnf(refute_0_7,plain,
( ~ p1(skolemFOFtoCNF_X_2)
| ~ p2(skolemFOFtoCNF_X_2)
| ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2)
| ~ r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2) ),
inference(subst,[],[refute_0_6:[bind(X_97,$fot(skolemFOFtoCNF_X_2)),bind(X_99,$fot(skolemFOFtoCNF_Y_2))]]) ).
cnf(refute_0_8,plain,
( ~ p1(skolemFOFtoCNF_X_2)
| ~ p2(skolemFOFtoCNF_X_2)
| ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2) )],[refute_0_0,refute_0_7]) ).
cnf(refute_0_9,plain,
r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_10,plain,
( ~ p1(skolemFOFtoCNF_X_2)
| ~ p2(skolemFOFtoCNF_X_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2) )],[refute_0_9,refute_0_8]) ).
cnf(refute_0_11,plain,
( ~ p1(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y) ),
inference(canonicalize,[],[normalize_0_18]) ).
cnf(refute_0_12,plain,
( ~ p1(X_162)
| ~ p3(X_162)
| ~ r1(X_164,X_162)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_164)
| ~ r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1) ),
inference(subst,[],[refute_0_11:[bind(X,$fot(skolemFOFtoCNF_X_1)),bind(X0,$fot(X_162)),bind(Y,$fot(skolemFOFtoCNF_Y_1)),bind(Y0,$fot(X_164))]]) ).
cnf(refute_0_13,plain,
( ~ p1(X_162)
| ~ p3(X_162)
| ~ r1(X_164,X_162)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_164) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1) )],[refute_0_1,refute_0_12]) ).
cnf(refute_0_14,plain,
( ~ p1(X_162)
| ~ p3(X_162)
| ~ r1(X_164,X_162)
| ~ r1(skolemFOFtoCNF_X_1,X_164) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1) )],[refute_0_5,refute_0_13]) ).
cnf(refute_0_15,plain,
( ~ p1(skolemFOFtoCNF_X_2)
| ~ p3(skolemFOFtoCNF_X_2)
| ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2)
| ~ r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2) ),
inference(subst,[],[refute_0_14:[bind(X_162,$fot(skolemFOFtoCNF_X_2)),bind(X_164,$fot(skolemFOFtoCNF_Y_2))]]) ).
cnf(refute_0_16,plain,
( ~ p1(skolemFOFtoCNF_X_2)
| ~ p3(skolemFOFtoCNF_X_2)
| ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2) )],[refute_0_0,refute_0_15]) ).
cnf(refute_0_17,plain,
( ~ p1(skolemFOFtoCNF_X_2)
| ~ p3(skolemFOFtoCNF_X_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2) )],[refute_0_9,refute_0_16]) ).
cnf(refute_0_18,plain,
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y)
| p2(X0)
| p3(X0) ),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_19,plain,
( ~ r1(X_421,X_419)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_421)
| ~ r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1)
| p2(X_419)
| p3(X_419) ),
inference(subst,[],[refute_0_18:[bind(X,$fot(skolemFOFtoCNF_X_1)),bind(X0,$fot(X_419)),bind(Y,$fot(skolemFOFtoCNF_Y_1)),bind(Y0,$fot(X_421))]]) ).
cnf(refute_0_20,plain,
( ~ r1(X_421,X_419)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_421)
| p2(X_419)
| p3(X_419) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1) )],[refute_0_1,refute_0_19]) ).
cnf(refute_0_21,plain,
( ~ r1(X_421,X_419)
| ~ r1(skolemFOFtoCNF_X_1,X_421)
| p2(X_419)
| p3(X_419) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1) )],[refute_0_5,refute_0_20]) ).
cnf(refute_0_22,plain,
( ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2)
| ~ r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2)
| p2(skolemFOFtoCNF_X_2)
| p3(skolemFOFtoCNF_X_2) ),
inference(subst,[],[refute_0_21:[bind(X_419,$fot(skolemFOFtoCNF_X_2)),bind(X_421,$fot(skolemFOFtoCNF_Y_2))]]) ).
cnf(refute_0_23,plain,
( ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2)
| p2(skolemFOFtoCNF_X_2)
| p3(skolemFOFtoCNF_X_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2) )],[refute_0_0,refute_0_22]) ).
cnf(refute_0_24,plain,
( p2(skolemFOFtoCNF_X_2)
| p3(skolemFOFtoCNF_X_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2) )],[refute_0_9,refute_0_23]) ).
cnf(refute_0_25,plain,
( ~ p1(skolemFOFtoCNF_X_2)
| p2(skolemFOFtoCNF_X_2) ),
inference(resolve,[$cnf( p3(skolemFOFtoCNF_X_2) )],[refute_0_24,refute_0_17]) ).
cnf(refute_0_26,plain,
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y)
| p1(X0)
| p2(X0) ),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_27,plain,
( ~ r1(X_282,X_280)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_282)
| ~ r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1)
| p1(X_280)
| p2(X_280) ),
inference(subst,[],[refute_0_26:[bind(X,$fot(skolemFOFtoCNF_X_1)),bind(X0,$fot(X_280)),bind(Y,$fot(skolemFOFtoCNF_Y_1)),bind(Y0,$fot(X_282))]]) ).
cnf(refute_0_28,plain,
( ~ r1(X_282,X_280)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_282)
| p1(X_280)
| p2(X_280) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1) )],[refute_0_1,refute_0_27]) ).
cnf(refute_0_29,plain,
( ~ r1(X_282,X_280)
| ~ r1(skolemFOFtoCNF_X_1,X_282)
| p1(X_280)
| p2(X_280) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1) )],[refute_0_5,refute_0_28]) ).
cnf(refute_0_30,plain,
( ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2)
| ~ r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2)
| p1(skolemFOFtoCNF_X_2)
| p2(skolemFOFtoCNF_X_2) ),
inference(subst,[],[refute_0_29:[bind(X_280,$fot(skolemFOFtoCNF_X_2)),bind(X_282,$fot(skolemFOFtoCNF_Y_2))]]) ).
cnf(refute_0_31,plain,
( ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2)
| p1(skolemFOFtoCNF_X_2)
| p2(skolemFOFtoCNF_X_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2) )],[refute_0_0,refute_0_30]) ).
cnf(refute_0_32,plain,
( p1(skolemFOFtoCNF_X_2)
| p2(skolemFOFtoCNF_X_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2) )],[refute_0_9,refute_0_31]) ).
cnf(refute_0_33,plain,
( ~ p2(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y) ),
inference(canonicalize,[],[normalize_0_21]) ).
cnf(refute_0_34,plain,
( ~ p2(X_221)
| ~ p3(X_221)
| ~ r1(X_223,X_221)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_223)
| ~ r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1) ),
inference(subst,[],[refute_0_33:[bind(X,$fot(skolemFOFtoCNF_X_1)),bind(X0,$fot(X_221)),bind(Y,$fot(skolemFOFtoCNF_Y_1)),bind(Y0,$fot(X_223))]]) ).
cnf(refute_0_35,plain,
( ~ p2(X_221)
| ~ p3(X_221)
| ~ r1(X_223,X_221)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_223) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1) )],[refute_0_1,refute_0_34]) ).
cnf(refute_0_36,plain,
( ~ p2(X_221)
| ~ p3(X_221)
| ~ r1(X_223,X_221)
| ~ r1(skolemFOFtoCNF_X_1,X_223) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1) )],[refute_0_5,refute_0_35]) ).
cnf(refute_0_37,plain,
( ~ p2(skolemFOFtoCNF_X_2)
| ~ p3(skolemFOFtoCNF_X_2)
| ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2)
| ~ r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2) ),
inference(subst,[],[refute_0_36:[bind(X_221,$fot(skolemFOFtoCNF_X_2)),bind(X_223,$fot(skolemFOFtoCNF_Y_2))]]) ).
cnf(refute_0_38,plain,
( ~ p2(skolemFOFtoCNF_X_2)
| ~ p3(skolemFOFtoCNF_X_2)
| ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2) )],[refute_0_0,refute_0_37]) ).
cnf(refute_0_39,plain,
( ~ p2(skolemFOFtoCNF_X_2)
| ~ p3(skolemFOFtoCNF_X_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2) )],[refute_0_9,refute_0_38]) ).
cnf(refute_0_40,plain,
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X,Y)
| p1(X0)
| p3(X0) ),
inference(canonicalize,[],[normalize_0_22]) ).
cnf(refute_0_41,plain,
( ~ r1(X_347,X_345)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_347)
| ~ r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1)
| p1(X_345)
| p3(X_345) ),
inference(subst,[],[refute_0_40:[bind(X,$fot(skolemFOFtoCNF_X_1)),bind(X0,$fot(X_345)),bind(Y,$fot(skolemFOFtoCNF_Y_1)),bind(Y0,$fot(X_347))]]) ).
cnf(refute_0_42,plain,
( ~ r1(X_347,X_345)
| ~ r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1)
| ~ r1(skolemFOFtoCNF_X_1,X_347)
| p1(X_345)
| p3(X_345) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_1,skolemFOFtoCNF_X_1) )],[refute_0_1,refute_0_41]) ).
cnf(refute_0_43,plain,
( ~ r1(X_347,X_345)
| ~ r1(skolemFOFtoCNF_X_1,X_347)
| p1(X_345)
| p3(X_345) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X,skolemFOFtoCNF_Y_1) )],[refute_0_5,refute_0_42]) ).
cnf(refute_0_44,plain,
( ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2)
| ~ r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2)
| p1(skolemFOFtoCNF_X_2)
| p3(skolemFOFtoCNF_X_2) ),
inference(subst,[],[refute_0_43:[bind(X_345,$fot(skolemFOFtoCNF_X_2)),bind(X_347,$fot(skolemFOFtoCNF_Y_2))]]) ).
cnf(refute_0_45,plain,
( ~ r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2)
| p1(skolemFOFtoCNF_X_2)
| p3(skolemFOFtoCNF_X_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_2,skolemFOFtoCNF_X_2) )],[refute_0_0,refute_0_44]) ).
cnf(refute_0_46,plain,
( p1(skolemFOFtoCNF_X_2)
| p3(skolemFOFtoCNF_X_2) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_2) )],[refute_0_9,refute_0_45]) ).
cnf(refute_0_47,plain,
( ~ p2(skolemFOFtoCNF_X_2)
| p1(skolemFOFtoCNF_X_2) ),
inference(resolve,[$cnf( p3(skolemFOFtoCNF_X_2) )],[refute_0_46,refute_0_39]) ).
cnf(refute_0_48,plain,
p1(skolemFOFtoCNF_X_2),
inference(resolve,[$cnf( p2(skolemFOFtoCNF_X_2) )],[refute_0_32,refute_0_47]) ).
cnf(refute_0_49,plain,
p2(skolemFOFtoCNF_X_2),
inference(resolve,[$cnf( p1(skolemFOFtoCNF_X_2) )],[refute_0_48,refute_0_25]) ).
cnf(refute_0_50,plain,
~ p1(skolemFOFtoCNF_X_2),
inference(resolve,[$cnf( p2(skolemFOFtoCNF_X_2) )],[refute_0_49,refute_0_10]) ).
cnf(refute_0_51,plain,
$false,
inference(resolve,[$cnf( p1(skolemFOFtoCNF_X_2) )],[refute_0_48,refute_0_50]) ).
fof(negate_1_0,plain,
~ ! [X] :
( ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ~ p8(X)
& ~ p6(X)
& ~ p4(X)
& ~ p2(X) ) ) ) ) )
& ~ ! [Y] :
( ~ r1(X,Y)
| p5(Y) )
& ~ ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ~ ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p3(X)
& ~ p1(X) )
| ( p1(X)
& p3(X) ) ) ) ) )
| ! [X] :
( ~ r1(Y,X)
| p4(X) )
| ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p2(X)
& ~ p3(X) )
| ( p3(X)
& p2(X) ) ) ) )
| ! [Y] :
( ~ r1(X,Y)
| p3(Y) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p1(X)
& ~ p2(X) )
| ( p2(X)
& p1(X) ) ) ) ) ) ) ) ) )
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ~ ~ r1(Y,X)
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ( ~ ~ r1(Y,X)
& p4(X) )
=> p3(X) ) ) ) ) ),
inference(negate,[],[subgoal_1]) ).
fof(normalize_1_0,plain,
? [X] :
( ? [Y] :
( ~ p5(Y)
& r1(X,Y) )
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ) )
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p3(X)
& p4(X)
& r1(Y,X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ) ),
inference(canonicalize,[],[negate_1_0]) ).
fof(normalize_1_1,plain,
( ? [Y] :
( ~ p5(Y)
& r1(skolemFOFtoCNF_X_6,Y) )
& ? [Y] :
( r1(skolemFOFtoCNF_X_6,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ) )
& ? [Y] :
( r1(skolemFOFtoCNF_X_6,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p3(X)
& p4(X)
& r1(Y,X) ) ) ) )
& ! [Y] :
( ~ r1(skolemFOFtoCNF_X_6,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ) ),
inference(skolemize,[],[normalize_1_0]) ).
fof(normalize_1_2,plain,
? [Y] :
( r1(skolemFOFtoCNF_X_6,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ) ),
inference(conjunct,[],[normalize_1_1]) ).
fof(normalize_1_3,plain,
( r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
& ? [X] :
( r1(skolemFOFtoCNF_Y_7,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ) ),
inference(skolemize,[],[normalize_1_2]) ).
fof(normalize_1_4,plain,
? [X] :
( r1(skolemFOFtoCNF_Y_7,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ),
inference(conjunct,[],[normalize_1_3]) ).
fof(normalize_1_5,plain,
( r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7)
& ? [Y] :
( r1(skolemFOFtoCNF_X_7,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ),
inference(skolemize,[],[normalize_1_4]) ).
fof(normalize_1_6,plain,
? [Y] :
( r1(skolemFOFtoCNF_X_7,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ),
inference(conjunct,[],[normalize_1_5]) ).
fof(normalize_1_7,plain,
( r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8)
& ? [X] :
( r1(skolemFOFtoCNF_Y_8,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ),
inference(skolemize,[],[normalize_1_6]) ).
fof(normalize_1_8,plain,
? [X] :
( r1(skolemFOFtoCNF_Y_8,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ),
inference(conjunct,[],[normalize_1_7]) ).
fof(normalize_1_9,plain,
( r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8)
& ( p2(skolemFOFtoCNF_X_8)
| p4(skolemFOFtoCNF_X_8)
| p6(skolemFOFtoCNF_X_8)
| p8(skolemFOFtoCNF_X_8) ) ),
inference(skolemize,[],[normalize_1_8]) ).
fof(normalize_1_10,plain,
r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8),
inference(conjunct,[],[normalize_1_9]) ).
fof(normalize_1_11,plain,
r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7),
inference(conjunct,[],[normalize_1_5]) ).
fof(normalize_1_12,plain,
! [Y] :
( ~ r1(skolemFOFtoCNF_X_6,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ),
inference(conjunct,[],[normalize_1_1]) ).
fof(normalize_1_13,plain,
! [Y] :
( ~ r1(skolemFOFtoCNF_X_6,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ),
inference(specialize,[],[normalize_1_12]) ).
fof(normalize_1_14,plain,
! [X,X0,Y,Y0] :
( ( ~ p4(skolemFOFtoCNF_X_11(Y))
| ~ r1(skolemFOFtoCNF_X_6,Y) )
& ( ~ r1(skolemFOFtoCNF_X_6,Y)
| r1(Y,skolemFOFtoCNF_X_11(Y)) )
& ( ~ p3(skolemFOFtoCNF_Y_11(X))
| ~ r1(Y,X)
| ~ r1(skolemFOFtoCNF_X_6,Y) )
& ( ~ r1(Y,X)
| ~ r1(skolemFOFtoCNF_X_6,Y)
| r1(X,skolemFOFtoCNF_Y_11(X)) )
& ( ~ p1(X0)
| ~ p2(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y) )
& ( ~ p1(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y) )
& ( ~ p2(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y)
| p1(X0)
| p2(X0) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y)
| p1(X0)
| p3(X0) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y)
| p2(X0)
| p3(X0) ) ),
inference(clausify,[],[normalize_1_13]) ).
fof(normalize_1_15,plain,
! [X,X0,Y,Y0] :
( ~ p1(X0)
| ~ p2(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y) ),
inference(conjunct,[],[normalize_1_14]) ).
fof(normalize_1_16,plain,
r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7),
inference(conjunct,[],[normalize_1_3]) ).
fof(normalize_1_17,plain,
r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8),
inference(conjunct,[],[normalize_1_7]) ).
fof(normalize_1_18,plain,
! [X,X0,Y,Y0] :
( ~ p1(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y) ),
inference(conjunct,[],[normalize_1_14]) ).
fof(normalize_1_19,plain,
! [X,X0,Y,Y0] :
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y)
| p2(X0)
| p3(X0) ),
inference(conjunct,[],[normalize_1_14]) ).
fof(normalize_1_20,plain,
! [X,X0,Y,Y0] :
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y)
| p1(X0)
| p2(X0) ),
inference(conjunct,[],[normalize_1_14]) ).
fof(normalize_1_21,plain,
! [X,X0,Y,Y0] :
( ~ p2(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y) ),
inference(conjunct,[],[normalize_1_14]) ).
fof(normalize_1_22,plain,
! [X,X0,Y,Y0] :
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y)
| p1(X0)
| p3(X0) ),
inference(conjunct,[],[normalize_1_14]) ).
cnf(refute_1_0,plain,
r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8),
inference(canonicalize,[],[normalize_1_10]) ).
cnf(refute_1_1,plain,
r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7),
inference(canonicalize,[],[normalize_1_11]) ).
cnf(refute_1_2,plain,
( ~ p1(X0)
| ~ p2(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y) ),
inference(canonicalize,[],[normalize_1_15]) ).
cnf(refute_1_3,plain,
( ~ p1(X_521)
| ~ p2(X_521)
| ~ r1(X_523,X_521)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_523)
| ~ r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7) ),
inference(subst,[],[refute_1_2:[bind(X,$fot(skolemFOFtoCNF_X_7)),bind(X0,$fot(X_521)),bind(Y,$fot(skolemFOFtoCNF_Y_7)),bind(Y0,$fot(X_523))]]) ).
cnf(refute_1_4,plain,
( ~ p1(X_521)
| ~ p2(X_521)
| ~ r1(X_523,X_521)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_523) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7) )],[refute_1_1,refute_1_3]) ).
cnf(refute_1_5,plain,
r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7),
inference(canonicalize,[],[normalize_1_16]) ).
cnf(refute_1_6,plain,
( ~ p1(X_521)
| ~ p2(X_521)
| ~ r1(X_523,X_521)
| ~ r1(skolemFOFtoCNF_X_7,X_523) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7) )],[refute_1_5,refute_1_4]) ).
cnf(refute_1_7,plain,
( ~ p1(skolemFOFtoCNF_X_8)
| ~ p2(skolemFOFtoCNF_X_8)
| ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8)
| ~ r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8) ),
inference(subst,[],[refute_1_6:[bind(X_521,$fot(skolemFOFtoCNF_X_8)),bind(X_523,$fot(skolemFOFtoCNF_Y_8))]]) ).
cnf(refute_1_8,plain,
( ~ p1(skolemFOFtoCNF_X_8)
| ~ p2(skolemFOFtoCNF_X_8)
| ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8) )],[refute_1_0,refute_1_7]) ).
cnf(refute_1_9,plain,
r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8),
inference(canonicalize,[],[normalize_1_17]) ).
cnf(refute_1_10,plain,
( ~ p1(skolemFOFtoCNF_X_8)
| ~ p2(skolemFOFtoCNF_X_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8) )],[refute_1_9,refute_1_8]) ).
cnf(refute_1_11,plain,
( ~ p1(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y) ),
inference(canonicalize,[],[normalize_1_18]) ).
cnf(refute_1_12,plain,
( ~ p1(X_587)
| ~ p3(X_587)
| ~ r1(X_589,X_587)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_589)
| ~ r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7) ),
inference(subst,[],[refute_1_11:[bind(X,$fot(skolemFOFtoCNF_X_7)),bind(X0,$fot(X_587)),bind(Y,$fot(skolemFOFtoCNF_Y_7)),bind(Y0,$fot(X_589))]]) ).
cnf(refute_1_13,plain,
( ~ p1(X_587)
| ~ p3(X_587)
| ~ r1(X_589,X_587)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_589) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7) )],[refute_1_1,refute_1_12]) ).
cnf(refute_1_14,plain,
( ~ p1(X_587)
| ~ p3(X_587)
| ~ r1(X_589,X_587)
| ~ r1(skolemFOFtoCNF_X_7,X_589) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7) )],[refute_1_5,refute_1_13]) ).
cnf(refute_1_15,plain,
( ~ p1(skolemFOFtoCNF_X_8)
| ~ p3(skolemFOFtoCNF_X_8)
| ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8)
| ~ r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8) ),
inference(subst,[],[refute_1_14:[bind(X_587,$fot(skolemFOFtoCNF_X_8)),bind(X_589,$fot(skolemFOFtoCNF_Y_8))]]) ).
cnf(refute_1_16,plain,
( ~ p1(skolemFOFtoCNF_X_8)
| ~ p3(skolemFOFtoCNF_X_8)
| ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8) )],[refute_1_0,refute_1_15]) ).
cnf(refute_1_17,plain,
( ~ p1(skolemFOFtoCNF_X_8)
| ~ p3(skolemFOFtoCNF_X_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8) )],[refute_1_9,refute_1_16]) ).
cnf(refute_1_18,plain,
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y)
| p2(X0)
| p3(X0) ),
inference(canonicalize,[],[normalize_1_19]) ).
cnf(refute_1_19,plain,
( ~ r1(X_850,X_848)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_850)
| ~ r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7)
| p2(X_848)
| p3(X_848) ),
inference(subst,[],[refute_1_18:[bind(X,$fot(skolemFOFtoCNF_X_7)),bind(X0,$fot(X_848)),bind(Y,$fot(skolemFOFtoCNF_Y_7)),bind(Y0,$fot(X_850))]]) ).
cnf(refute_1_20,plain,
( ~ r1(X_850,X_848)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_850)
| p2(X_848)
| p3(X_848) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7) )],[refute_1_1,refute_1_19]) ).
cnf(refute_1_21,plain,
( ~ r1(X_850,X_848)
| ~ r1(skolemFOFtoCNF_X_7,X_850)
| p2(X_848)
| p3(X_848) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7) )],[refute_1_5,refute_1_20]) ).
cnf(refute_1_22,plain,
( ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8)
| ~ r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8)
| p2(skolemFOFtoCNF_X_8)
| p3(skolemFOFtoCNF_X_8) ),
inference(subst,[],[refute_1_21:[bind(X_848,$fot(skolemFOFtoCNF_X_8)),bind(X_850,$fot(skolemFOFtoCNF_Y_8))]]) ).
cnf(refute_1_23,plain,
( ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8)
| p2(skolemFOFtoCNF_X_8)
| p3(skolemFOFtoCNF_X_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8) )],[refute_1_0,refute_1_22]) ).
cnf(refute_1_24,plain,
( p2(skolemFOFtoCNF_X_8)
| p3(skolemFOFtoCNF_X_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8) )],[refute_1_9,refute_1_23]) ).
cnf(refute_1_25,plain,
( ~ p1(skolemFOFtoCNF_X_8)
| p2(skolemFOFtoCNF_X_8) ),
inference(resolve,[$cnf( p3(skolemFOFtoCNF_X_8) )],[refute_1_24,refute_1_17]) ).
cnf(refute_1_26,plain,
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y)
| p1(X0)
| p2(X0) ),
inference(canonicalize,[],[normalize_1_20]) ).
cnf(refute_1_27,plain,
( ~ r1(X_709,X_707)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_709)
| ~ r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7)
| p1(X_707)
| p2(X_707) ),
inference(subst,[],[refute_1_26:[bind(X,$fot(skolemFOFtoCNF_X_7)),bind(X0,$fot(X_707)),bind(Y,$fot(skolemFOFtoCNF_Y_7)),bind(Y0,$fot(X_709))]]) ).
cnf(refute_1_28,plain,
( ~ r1(X_709,X_707)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_709)
| p1(X_707)
| p2(X_707) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7) )],[refute_1_1,refute_1_27]) ).
cnf(refute_1_29,plain,
( ~ r1(X_709,X_707)
| ~ r1(skolemFOFtoCNF_X_7,X_709)
| p1(X_707)
| p2(X_707) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7) )],[refute_1_5,refute_1_28]) ).
cnf(refute_1_30,plain,
( ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8)
| ~ r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8)
| p1(skolemFOFtoCNF_X_8)
| p2(skolemFOFtoCNF_X_8) ),
inference(subst,[],[refute_1_29:[bind(X_707,$fot(skolemFOFtoCNF_X_8)),bind(X_709,$fot(skolemFOFtoCNF_Y_8))]]) ).
cnf(refute_1_31,plain,
( ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8)
| p1(skolemFOFtoCNF_X_8)
| p2(skolemFOFtoCNF_X_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8) )],[refute_1_0,refute_1_30]) ).
cnf(refute_1_32,plain,
( p1(skolemFOFtoCNF_X_8)
| p2(skolemFOFtoCNF_X_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8) )],[refute_1_9,refute_1_31]) ).
cnf(refute_1_33,plain,
( ~ p2(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y) ),
inference(canonicalize,[],[normalize_1_21]) ).
cnf(refute_1_34,plain,
( ~ p2(X_647)
| ~ p3(X_647)
| ~ r1(X_649,X_647)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_649)
| ~ r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7) ),
inference(subst,[],[refute_1_33:[bind(X,$fot(skolemFOFtoCNF_X_7)),bind(X0,$fot(X_647)),bind(Y,$fot(skolemFOFtoCNF_Y_7)),bind(Y0,$fot(X_649))]]) ).
cnf(refute_1_35,plain,
( ~ p2(X_647)
| ~ p3(X_647)
| ~ r1(X_649,X_647)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_649) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7) )],[refute_1_1,refute_1_34]) ).
cnf(refute_1_36,plain,
( ~ p2(X_647)
| ~ p3(X_647)
| ~ r1(X_649,X_647)
| ~ r1(skolemFOFtoCNF_X_7,X_649) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7) )],[refute_1_5,refute_1_35]) ).
cnf(refute_1_37,plain,
( ~ p2(skolemFOFtoCNF_X_8)
| ~ p3(skolemFOFtoCNF_X_8)
| ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8)
| ~ r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8) ),
inference(subst,[],[refute_1_36:[bind(X_647,$fot(skolemFOFtoCNF_X_8)),bind(X_649,$fot(skolemFOFtoCNF_Y_8))]]) ).
cnf(refute_1_38,plain,
( ~ p2(skolemFOFtoCNF_X_8)
| ~ p3(skolemFOFtoCNF_X_8)
| ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8) )],[refute_1_0,refute_1_37]) ).
cnf(refute_1_39,plain,
( ~ p2(skolemFOFtoCNF_X_8)
| ~ p3(skolemFOFtoCNF_X_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8) )],[refute_1_9,refute_1_38]) ).
cnf(refute_1_40,plain,
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_6,Y)
| p1(X0)
| p3(X0) ),
inference(canonicalize,[],[normalize_1_22]) ).
cnf(refute_1_41,plain,
( ~ r1(X_775,X_773)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_775)
| ~ r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7)
| p1(X_773)
| p3(X_773) ),
inference(subst,[],[refute_1_40:[bind(X,$fot(skolemFOFtoCNF_X_7)),bind(X0,$fot(X_773)),bind(Y,$fot(skolemFOFtoCNF_Y_7)),bind(Y0,$fot(X_775))]]) ).
cnf(refute_1_42,plain,
( ~ r1(X_775,X_773)
| ~ r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7)
| ~ r1(skolemFOFtoCNF_X_7,X_775)
| p1(X_773)
| p3(X_773) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_7,skolemFOFtoCNF_X_7) )],[refute_1_1,refute_1_41]) ).
cnf(refute_1_43,plain,
( ~ r1(X_775,X_773)
| ~ r1(skolemFOFtoCNF_X_7,X_775)
| p1(X_773)
| p3(X_773) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_6,skolemFOFtoCNF_Y_7) )],[refute_1_5,refute_1_42]) ).
cnf(refute_1_44,plain,
( ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8)
| ~ r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8)
| p1(skolemFOFtoCNF_X_8)
| p3(skolemFOFtoCNF_X_8) ),
inference(subst,[],[refute_1_43:[bind(X_773,$fot(skolemFOFtoCNF_X_8)),bind(X_775,$fot(skolemFOFtoCNF_Y_8))]]) ).
cnf(refute_1_45,plain,
( ~ r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8)
| p1(skolemFOFtoCNF_X_8)
| p3(skolemFOFtoCNF_X_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_8,skolemFOFtoCNF_X_8) )],[refute_1_0,refute_1_44]) ).
cnf(refute_1_46,plain,
( p1(skolemFOFtoCNF_X_8)
| p3(skolemFOFtoCNF_X_8) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_8) )],[refute_1_9,refute_1_45]) ).
cnf(refute_1_47,plain,
( ~ p2(skolemFOFtoCNF_X_8)
| p1(skolemFOFtoCNF_X_8) ),
inference(resolve,[$cnf( p3(skolemFOFtoCNF_X_8) )],[refute_1_46,refute_1_39]) ).
cnf(refute_1_48,plain,
p1(skolemFOFtoCNF_X_8),
inference(resolve,[$cnf( p2(skolemFOFtoCNF_X_8) )],[refute_1_32,refute_1_47]) ).
cnf(refute_1_49,plain,
p2(skolemFOFtoCNF_X_8),
inference(resolve,[$cnf( p1(skolemFOFtoCNF_X_8) )],[refute_1_48,refute_1_25]) ).
cnf(refute_1_50,plain,
~ p1(skolemFOFtoCNF_X_8),
inference(resolve,[$cnf( p2(skolemFOFtoCNF_X_8) )],[refute_1_49,refute_1_10]) ).
cnf(refute_1_51,plain,
$false,
inference(resolve,[$cnf( p1(skolemFOFtoCNF_X_8) )],[refute_1_48,refute_1_50]) ).
fof(negate_2_0,plain,
~ ! [X] :
( ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ~ p8(X)
& ~ p6(X)
& ~ p4(X)
& ~ p2(X) ) ) ) ) )
& ~ ! [Y] :
( ~ r1(X,Y)
| p5(Y) )
& ~ ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ~ ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p3(X)
& ~ p1(X) )
| ( p1(X)
& p3(X) ) ) ) ) )
| ! [X] :
( ~ r1(Y,X)
| p4(X) )
| ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p2(X)
& ~ p3(X) )
| ( p3(X)
& p2(X) ) ) ) )
| ! [Y] :
( ~ r1(X,Y)
| p3(Y) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p1(X)
& ~ p2(X) )
| ( p2(X)
& p1(X) ) ) ) ) ) ) ) ) )
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ~ ~ r1(Y,X)
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ( ~ ~ r1(Y,X)
& p4(X)
& p3(X) )
=> p2(X) ) ) ) ) ),
inference(negate,[],[subgoal_2]) ).
fof(normalize_2_0,plain,
? [X] :
( ? [Y] :
( ~ p5(Y)
& r1(X,Y) )
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ) )
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ) ),
inference(canonicalize,[],[negate_2_0]) ).
fof(normalize_2_1,plain,
( ? [Y] :
( ~ p5(Y)
& r1(skolemFOFtoCNF_X_12,Y) )
& ? [Y] :
( r1(skolemFOFtoCNF_X_12,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ) )
& ? [Y] :
( r1(skolemFOFtoCNF_X_12,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ) )
& ! [Y] :
( ~ r1(skolemFOFtoCNF_X_12,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ) ),
inference(skolemize,[],[normalize_2_0]) ).
fof(normalize_2_2,plain,
? [Y] :
( r1(skolemFOFtoCNF_X_12,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ) ),
inference(conjunct,[],[normalize_2_1]) ).
fof(normalize_2_3,plain,
( r1(skolemFOFtoCNF_X_12,skolemFOFtoCNF_Y_15)
& ? [X] :
( r1(skolemFOFtoCNF_Y_15,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ) ),
inference(skolemize,[],[normalize_2_2]) ).
fof(normalize_2_4,plain,
? [X] :
( r1(skolemFOFtoCNF_Y_15,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ),
inference(conjunct,[],[normalize_2_3]) ).
fof(normalize_2_5,plain,
( r1(skolemFOFtoCNF_Y_15,skolemFOFtoCNF_X_15)
& ? [Y] :
( r1(skolemFOFtoCNF_X_15,Y)
& ? [X] :
( ~ p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ),
inference(skolemize,[],[normalize_2_4]) ).
fof(normalize_2_6,plain,
r1(skolemFOFtoCNF_Y_15,skolemFOFtoCNF_X_15),
inference(conjunct,[],[normalize_2_5]) ).
fof(normalize_2_7,plain,
? [Y] :
( r1(skolemFOFtoCNF_X_15,Y)
& ? [X] :
( ~ p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ),
inference(conjunct,[],[normalize_2_5]) ).
fof(normalize_2_8,plain,
( r1(skolemFOFtoCNF_X_15,skolemFOFtoCNF_Y_16)
& ? [X] :
( ~ p2(X)
& p3(X)
& p4(X)
& r1(skolemFOFtoCNF_Y_16,X) ) ),
inference(skolemize,[],[normalize_2_7]) ).
fof(normalize_2_9,plain,
? [X] :
( ~ p2(X)
& p3(X)
& p4(X)
& r1(skolemFOFtoCNF_Y_16,X) ),
inference(conjunct,[],[normalize_2_8]) ).
fof(normalize_2_10,plain,
( ~ p2(skolemFOFtoCNF_X_16)
& p3(skolemFOFtoCNF_X_16)
& p4(skolemFOFtoCNF_X_16)
& r1(skolemFOFtoCNF_Y_16,skolemFOFtoCNF_X_16) ),
inference(skolemize,[],[normalize_2_9]) ).
fof(normalize_2_11,plain,
r1(skolemFOFtoCNF_Y_16,skolemFOFtoCNF_X_16),
inference(conjunct,[],[normalize_2_10]) ).
fof(normalize_2_12,plain,
! [Y] :
( ~ r1(skolemFOFtoCNF_X_12,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ),
inference(conjunct,[],[normalize_2_1]) ).
fof(normalize_2_13,plain,
! [Y] :
( ~ r1(skolemFOFtoCNF_X_12,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ),
inference(specialize,[],[normalize_2_12]) ).
fof(normalize_2_14,plain,
! [X,X0,Y,Y0] :
( ( ~ p4(skolemFOFtoCNF_X_17(Y))
| ~ r1(skolemFOFtoCNF_X_12,Y) )
& ( ~ r1(skolemFOFtoCNF_X_12,Y)
| r1(Y,skolemFOFtoCNF_X_17(Y)) )
& ( ~ p3(skolemFOFtoCNF_Y_17(X))
| ~ r1(Y,X)
| ~ r1(skolemFOFtoCNF_X_12,Y) )
& ( ~ r1(Y,X)
| ~ r1(skolemFOFtoCNF_X_12,Y)
| r1(X,skolemFOFtoCNF_Y_17(X)) )
& ( ~ p1(X0)
| ~ p2(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_12,Y) )
& ( ~ p1(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_12,Y) )
& ( ~ p2(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_12,Y) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_12,Y)
| p1(X0)
| p2(X0) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_12,Y)
| p1(X0)
| p3(X0) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_12,Y)
| p2(X0)
| p3(X0) ) ),
inference(clausify,[],[normalize_2_13]) ).
fof(normalize_2_15,plain,
! [X,X0,Y,Y0] :
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_12,Y)
| p1(X0)
| p2(X0) ),
inference(conjunct,[],[normalize_2_14]) ).
fof(normalize_2_16,plain,
! [X,X0,Y,Y0] :
( ~ p1(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_12,Y) ),
inference(conjunct,[],[normalize_2_14]) ).
fof(normalize_2_17,plain,
r1(skolemFOFtoCNF_X_12,skolemFOFtoCNF_Y_15),
inference(conjunct,[],[normalize_2_3]) ).
fof(normalize_2_18,plain,
p3(skolemFOFtoCNF_X_16),
inference(conjunct,[],[normalize_2_10]) ).
fof(normalize_2_19,plain,
r1(skolemFOFtoCNF_X_15,skolemFOFtoCNF_Y_16),
inference(conjunct,[],[normalize_2_8]) ).
fof(normalize_2_20,plain,
~ p2(skolemFOFtoCNF_X_16),
inference(conjunct,[],[normalize_2_10]) ).
cnf(refute_2_0,plain,
r1(skolemFOFtoCNF_Y_15,skolemFOFtoCNF_X_15),
inference(canonicalize,[],[normalize_2_6]) ).
cnf(refute_2_1,plain,
r1(skolemFOFtoCNF_Y_16,skolemFOFtoCNF_X_16),
inference(canonicalize,[],[normalize_2_11]) ).
cnf(refute_2_2,plain,
( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_12,Y)
| p1(X0)
| p2(X0) ),
inference(canonicalize,[],[normalize_2_15]) ).
cnf(refute_2_3,plain,
( ~ r1(X_1132,skolemFOFtoCNF_Y_16)
| ~ r1(X_1134,X_1132)
| ~ r1(skolemFOFtoCNF_X_12,X_1134)
| ~ r1(skolemFOFtoCNF_Y_16,skolemFOFtoCNF_X_16)
| p1(skolemFOFtoCNF_X_16)
| p2(skolemFOFtoCNF_X_16) ),
inference(subst,[],[refute_2_2:[bind(X,$fot(X_1132)),bind(X0,$fot(skolemFOFtoCNF_X_16)),bind(Y,$fot(X_1134)),bind(Y0,$fot(skolemFOFtoCNF_Y_16))]]) ).
cnf(refute_2_4,plain,
( ~ r1(X_1132,skolemFOFtoCNF_Y_16)
| ~ r1(X_1134,X_1132)
| ~ r1(skolemFOFtoCNF_X_12,X_1134)
| p1(skolemFOFtoCNF_X_16)
| p2(skolemFOFtoCNF_X_16) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_16,skolemFOFtoCNF_X_16) )],[refute_2_1,refute_2_3]) ).
cnf(refute_2_5,plain,
( ~ p1(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_12,Y) ),
inference(canonicalize,[],[normalize_2_16]) ).
cnf(refute_2_6,plain,
( ~ p1(X_1015)
| ~ p3(X_1015)
| ~ r1(X_1017,X_1015)
| ~ r1(skolemFOFtoCNF_X_12,skolemFOFtoCNF_Y_15)
| ~ r1(skolemFOFtoCNF_X_15,X_1017)
| ~ r1(skolemFOFtoCNF_Y_15,skolemFOFtoCNF_X_15) ),
inference(subst,[],[refute_2_5:[bind(X,$fot(skolemFOFtoCNF_X_15)),bind(X0,$fot(X_1015)),bind(Y,$fot(skolemFOFtoCNF_Y_15)),bind(Y0,$fot(X_1017))]]) ).
cnf(refute_2_7,plain,
( ~ p1(X_1015)
| ~ p3(X_1015)
| ~ r1(X_1017,X_1015)
| ~ r1(skolemFOFtoCNF_X_12,skolemFOFtoCNF_Y_15)
| ~ r1(skolemFOFtoCNF_X_15,X_1017) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_15,skolemFOFtoCNF_X_15) )],[refute_2_0,refute_2_6]) ).
cnf(refute_2_8,plain,
r1(skolemFOFtoCNF_X_12,skolemFOFtoCNF_Y_15),
inference(canonicalize,[],[normalize_2_17]) ).
cnf(refute_2_9,plain,
( ~ p1(X_1015)
| ~ p3(X_1015)
| ~ r1(X_1017,X_1015)
| ~ r1(skolemFOFtoCNF_X_15,X_1017) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_12,skolemFOFtoCNF_Y_15) )],[refute_2_8,refute_2_7]) ).
cnf(refute_2_10,plain,
( ~ p1(skolemFOFtoCNF_X_16)
| ~ p3(skolemFOFtoCNF_X_16)
| ~ r1(skolemFOFtoCNF_X_15,skolemFOFtoCNF_Y_16)
| ~ r1(skolemFOFtoCNF_Y_16,skolemFOFtoCNF_X_16) ),
inference(subst,[],[refute_2_9:[bind(X_1015,$fot(skolemFOFtoCNF_X_16)),bind(X_1017,$fot(skolemFOFtoCNF_Y_16))]]) ).
cnf(refute_2_11,plain,
( ~ p1(skolemFOFtoCNF_X_16)
| ~ p3(skolemFOFtoCNF_X_16)
| ~ r1(skolemFOFtoCNF_X_15,skolemFOFtoCNF_Y_16) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_16,skolemFOFtoCNF_X_16) )],[refute_2_1,refute_2_10]) ).
cnf(refute_2_12,plain,
p3(skolemFOFtoCNF_X_16),
inference(canonicalize,[],[normalize_2_18]) ).
cnf(refute_2_13,plain,
( ~ p1(skolemFOFtoCNF_X_16)
| ~ r1(skolemFOFtoCNF_X_15,skolemFOFtoCNF_Y_16) ),
inference(resolve,[$cnf( p3(skolemFOFtoCNF_X_16) )],[refute_2_12,refute_2_11]) ).
cnf(refute_2_14,plain,
r1(skolemFOFtoCNF_X_15,skolemFOFtoCNF_Y_16),
inference(canonicalize,[],[normalize_2_19]) ).
cnf(refute_2_15,plain,
~ p1(skolemFOFtoCNF_X_16),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_15,skolemFOFtoCNF_Y_16) )],[refute_2_14,refute_2_13]) ).
cnf(refute_2_16,plain,
( ~ r1(X_1132,skolemFOFtoCNF_Y_16)
| ~ r1(X_1134,X_1132)
| ~ r1(skolemFOFtoCNF_X_12,X_1134)
| p2(skolemFOFtoCNF_X_16) ),
inference(resolve,[$cnf( p1(skolemFOFtoCNF_X_16) )],[refute_2_4,refute_2_15]) ).
cnf(refute_2_17,plain,
~ p2(skolemFOFtoCNF_X_16),
inference(canonicalize,[],[normalize_2_20]) ).
cnf(refute_2_18,plain,
( ~ r1(X_1132,skolemFOFtoCNF_Y_16)
| ~ r1(X_1134,X_1132)
| ~ r1(skolemFOFtoCNF_X_12,X_1134) ),
inference(resolve,[$cnf( p2(skolemFOFtoCNF_X_16) )],[refute_2_16,refute_2_17]) ).
cnf(refute_2_19,plain,
( ~ r1(skolemFOFtoCNF_X_12,skolemFOFtoCNF_Y_15)
| ~ r1(skolemFOFtoCNF_X_15,skolemFOFtoCNF_Y_16)
| ~ r1(skolemFOFtoCNF_Y_15,skolemFOFtoCNF_X_15) ),
inference(subst,[],[refute_2_18:[bind(X_1132,$fot(skolemFOFtoCNF_X_15)),bind(X_1134,$fot(skolemFOFtoCNF_Y_15))]]) ).
cnf(refute_2_20,plain,
( ~ r1(skolemFOFtoCNF_X_12,skolemFOFtoCNF_Y_15)
| ~ r1(skolemFOFtoCNF_X_15,skolemFOFtoCNF_Y_16) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_15,skolemFOFtoCNF_X_15) )],[refute_2_0,refute_2_19]) ).
cnf(refute_2_21,plain,
~ r1(skolemFOFtoCNF_X_15,skolemFOFtoCNF_Y_16),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_12,skolemFOFtoCNF_Y_15) )],[refute_2_8,refute_2_20]) ).
cnf(refute_2_22,plain,
$false,
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_15,skolemFOFtoCNF_Y_16) )],[refute_2_14,refute_2_21]) ).
fof(negate_3_0,plain,
~ ! [X] :
( ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ~ p8(X)
& ~ p6(X)
& ~ p4(X)
& ~ p2(X) ) ) ) ) )
& ~ ! [Y] :
( ~ r1(X,Y)
| p5(Y) )
& ~ ~ ! [Y] :
( ~ r1(X,Y)
| ~ ( ~ ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p3(X)
& ~ p1(X) )
| ( p1(X)
& p3(X) ) ) ) ) )
| ! [X] :
( ~ r1(Y,X)
| p4(X) )
| ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ~ ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p2(X)
& ~ p3(X) )
| ( p3(X)
& p2(X) ) ) ) )
| ! [Y] :
( ~ r1(X,Y)
| p3(Y) )
| ~ ! [Y] :
( ~ r1(X,Y)
| ~ ~ ! [X] :
( ~ r1(Y,X)
| ~ ( ( ~ p1(X)
& ~ p2(X) )
| ( p2(X)
& p1(X) ) ) ) ) ) ) ) ) )
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ~ ~ r1(Y,X)
=> ! [Y] :
( ~ ~ r1(X,Y)
=> ! [X] :
( ( ~ ~ r1(Y,X)
& p4(X)
& p3(X)
& p2(X) )
=> p1(X) ) ) ) ) ),
inference(negate,[],[subgoal_3]) ).
fof(normalize_3_0,plain,
? [X] :
( ? [Y] :
( ~ p5(Y)
& r1(X,Y) )
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ) )
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p1(X)
& p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ) ),
inference(canonicalize,[],[negate_3_0]) ).
fof(normalize_3_1,plain,
( ? [Y] :
( ~ p5(Y)
& r1(skolemFOFtoCNF_X_18,Y) )
& ? [Y] :
( r1(skolemFOFtoCNF_X_18,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( r1(Y,X)
& ( p2(X)
| p4(X)
| p6(X)
| p8(X) ) ) ) ) )
& ? [Y] :
( r1(skolemFOFtoCNF_X_18,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p1(X)
& p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ) )
& ! [Y] :
( ~ r1(skolemFOFtoCNF_X_18,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ) ),
inference(skolemize,[],[normalize_3_0]) ).
fof(normalize_3_2,plain,
? [Y] :
( r1(skolemFOFtoCNF_X_18,Y)
& ? [X] :
( r1(Y,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p1(X)
& p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ) ),
inference(conjunct,[],[normalize_3_1]) ).
fof(normalize_3_3,plain,
( r1(skolemFOFtoCNF_X_18,skolemFOFtoCNF_Y_21)
& ? [X] :
( r1(skolemFOFtoCNF_Y_21,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p1(X)
& p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ) ),
inference(skolemize,[],[normalize_3_2]) ).
fof(normalize_3_4,plain,
? [X] :
( r1(skolemFOFtoCNF_Y_21,X)
& ? [Y] :
( r1(X,Y)
& ? [X] :
( ~ p1(X)
& p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ),
inference(conjunct,[],[normalize_3_3]) ).
fof(normalize_3_5,plain,
( r1(skolemFOFtoCNF_Y_21,skolemFOFtoCNF_X_21)
& ? [Y] :
( r1(skolemFOFtoCNF_X_21,Y)
& ? [X] :
( ~ p1(X)
& p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ) ),
inference(skolemize,[],[normalize_3_4]) ).
fof(normalize_3_6,plain,
r1(skolemFOFtoCNF_Y_21,skolemFOFtoCNF_X_21),
inference(conjunct,[],[normalize_3_5]) ).
fof(normalize_3_7,plain,
? [Y] :
( r1(skolemFOFtoCNF_X_21,Y)
& ? [X] :
( ~ p1(X)
& p2(X)
& p3(X)
& p4(X)
& r1(Y,X) ) ),
inference(conjunct,[],[normalize_3_5]) ).
fof(normalize_3_8,plain,
( r1(skolemFOFtoCNF_X_21,skolemFOFtoCNF_Y_22)
& ? [X] :
( ~ p1(X)
& p2(X)
& p3(X)
& p4(X)
& r1(skolemFOFtoCNF_Y_22,X) ) ),
inference(skolemize,[],[normalize_3_7]) ).
fof(normalize_3_9,plain,
? [X] :
( ~ p1(X)
& p2(X)
& p3(X)
& p4(X)
& r1(skolemFOFtoCNF_Y_22,X) ),
inference(conjunct,[],[normalize_3_8]) ).
fof(normalize_3_10,plain,
( ~ p1(skolemFOFtoCNF_X_22)
& p2(skolemFOFtoCNF_X_22)
& p3(skolemFOFtoCNF_X_22)
& p4(skolemFOFtoCNF_X_22)
& r1(skolemFOFtoCNF_Y_22,skolemFOFtoCNF_X_22) ),
inference(skolemize,[],[normalize_3_9]) ).
fof(normalize_3_11,plain,
r1(skolemFOFtoCNF_Y_22,skolemFOFtoCNF_X_22),
inference(conjunct,[],[normalize_3_10]) ).
fof(normalize_3_12,plain,
! [Y] :
( ~ r1(skolemFOFtoCNF_X_18,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ),
inference(conjunct,[],[normalize_3_1]) ).
fof(normalize_3_13,plain,
! [Y] :
( ~ r1(skolemFOFtoCNF_X_18,Y)
| ( ? [X] :
( ~ p4(X)
& r1(Y,X) )
& ! [X] :
( ~ r1(Y,X)
| ( ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p2(X) )
& ( p1(X)
| p2(X) ) ) ) )
& ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p2(X)
| ~ p3(X) )
& ( p2(X)
| p3(X) ) ) ) ) ) )
& ! [X] :
( ~ r1(Y,X)
| ! [Y] :
( ~ r1(X,Y)
| ! [X] :
( ~ r1(Y,X)
| ( ( ~ p1(X)
| ~ p3(X) )
& ( p1(X)
| p3(X) ) ) ) ) ) ) ),
inference(specialize,[],[normalize_3_12]) ).
fof(normalize_3_14,plain,
! [X,X0,Y,Y0] :
( ( ~ p4(skolemFOFtoCNF_X_23(Y))
| ~ r1(skolemFOFtoCNF_X_18,Y) )
& ( ~ r1(skolemFOFtoCNF_X_18,Y)
| r1(Y,skolemFOFtoCNF_X_23(Y)) )
& ( ~ p3(skolemFOFtoCNF_Y_23(X))
| ~ r1(Y,X)
| ~ r1(skolemFOFtoCNF_X_18,Y) )
& ( ~ r1(Y,X)
| ~ r1(skolemFOFtoCNF_X_18,Y)
| r1(X,skolemFOFtoCNF_Y_23(X)) )
& ( ~ p1(X0)
| ~ p2(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_18,Y) )
& ( ~ p1(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_18,Y) )
& ( ~ p2(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_18,Y) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_18,Y)
| p1(X0)
| p2(X0) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_18,Y)
| p1(X0)
| p3(X0) )
& ( ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_18,Y)
| p2(X0)
| p3(X0) ) ),
inference(clausify,[],[normalize_3_13]) ).
fof(normalize_3_15,plain,
! [X,X0,Y,Y0] :
( ~ p2(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_18,Y) ),
inference(conjunct,[],[normalize_3_14]) ).
fof(normalize_3_16,plain,
p2(skolemFOFtoCNF_X_22),
inference(conjunct,[],[normalize_3_10]) ).
fof(normalize_3_17,plain,
p3(skolemFOFtoCNF_X_22),
inference(conjunct,[],[normalize_3_10]) ).
fof(normalize_3_18,plain,
r1(skolemFOFtoCNF_X_18,skolemFOFtoCNF_Y_21),
inference(conjunct,[],[normalize_3_3]) ).
fof(normalize_3_19,plain,
r1(skolemFOFtoCNF_X_21,skolemFOFtoCNF_Y_22),
inference(conjunct,[],[normalize_3_8]) ).
cnf(refute_3_0,plain,
r1(skolemFOFtoCNF_Y_21,skolemFOFtoCNF_X_21),
inference(canonicalize,[],[normalize_3_6]) ).
cnf(refute_3_1,plain,
r1(skolemFOFtoCNF_Y_22,skolemFOFtoCNF_X_22),
inference(canonicalize,[],[normalize_3_11]) ).
cnf(refute_3_2,plain,
( ~ p2(X0)
| ~ p3(X0)
| ~ r1(X,Y0)
| ~ r1(Y,X)
| ~ r1(Y0,X0)
| ~ r1(skolemFOFtoCNF_X_18,Y) ),
inference(canonicalize,[],[normalize_3_15]) ).
cnf(refute_3_3,plain,
( ~ p2(skolemFOFtoCNF_X_22)
| ~ p3(skolemFOFtoCNF_X_22)
| ~ r1(X_1358,skolemFOFtoCNF_Y_22)
| ~ r1(X_1360,X_1358)
| ~ r1(skolemFOFtoCNF_X_18,X_1360)
| ~ r1(skolemFOFtoCNF_Y_22,skolemFOFtoCNF_X_22) ),
inference(subst,[],[refute_3_2:[bind(X,$fot(X_1358)),bind(X0,$fot(skolemFOFtoCNF_X_22)),bind(Y,$fot(X_1360)),bind(Y0,$fot(skolemFOFtoCNF_Y_22))]]) ).
cnf(refute_3_4,plain,
( ~ p2(skolemFOFtoCNF_X_22)
| ~ p3(skolemFOFtoCNF_X_22)
| ~ r1(X_1358,skolemFOFtoCNF_Y_22)
| ~ r1(X_1360,X_1358)
| ~ r1(skolemFOFtoCNF_X_18,X_1360) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_22,skolemFOFtoCNF_X_22) )],[refute_3_1,refute_3_3]) ).
cnf(refute_3_5,plain,
p2(skolemFOFtoCNF_X_22),
inference(canonicalize,[],[normalize_3_16]) ).
cnf(refute_3_6,plain,
( ~ p3(skolemFOFtoCNF_X_22)
| ~ r1(X_1358,skolemFOFtoCNF_Y_22)
| ~ r1(X_1360,X_1358)
| ~ r1(skolemFOFtoCNF_X_18,X_1360) ),
inference(resolve,[$cnf( p2(skolemFOFtoCNF_X_22) )],[refute_3_5,refute_3_4]) ).
cnf(refute_3_7,plain,
p3(skolemFOFtoCNF_X_22),
inference(canonicalize,[],[normalize_3_17]) ).
cnf(refute_3_8,plain,
( ~ r1(X_1358,skolemFOFtoCNF_Y_22)
| ~ r1(X_1360,X_1358)
| ~ r1(skolemFOFtoCNF_X_18,X_1360) ),
inference(resolve,[$cnf( p3(skolemFOFtoCNF_X_22) )],[refute_3_7,refute_3_6]) ).
cnf(refute_3_9,plain,
( ~ r1(skolemFOFtoCNF_X_18,skolemFOFtoCNF_Y_21)
| ~ r1(skolemFOFtoCNF_X_21,skolemFOFtoCNF_Y_22)
| ~ r1(skolemFOFtoCNF_Y_21,skolemFOFtoCNF_X_21) ),
inference(subst,[],[refute_3_8:[bind(X_1358,$fot(skolemFOFtoCNF_X_21)),bind(X_1360,$fot(skolemFOFtoCNF_Y_21))]]) ).
cnf(refute_3_10,plain,
( ~ r1(skolemFOFtoCNF_X_18,skolemFOFtoCNF_Y_21)
| ~ r1(skolemFOFtoCNF_X_21,skolemFOFtoCNF_Y_22) ),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_Y_21,skolemFOFtoCNF_X_21) )],[refute_3_0,refute_3_9]) ).
cnf(refute_3_11,plain,
r1(skolemFOFtoCNF_X_18,skolemFOFtoCNF_Y_21),
inference(canonicalize,[],[normalize_3_18]) ).
cnf(refute_3_12,plain,
~ r1(skolemFOFtoCNF_X_21,skolemFOFtoCNF_Y_22),
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_18,skolemFOFtoCNF_Y_21) )],[refute_3_11,refute_3_10]) ).
cnf(refute_3_13,plain,
r1(skolemFOFtoCNF_X_21,skolemFOFtoCNF_Y_22),
inference(canonicalize,[],[normalize_3_19]) ).
cnf(refute_3_14,plain,
$false,
inference(resolve,[$cnf( r1(skolemFOFtoCNF_X_21,skolemFOFtoCNF_Y_22) )],[refute_3_13,refute_3_12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL650+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : metis --show proof --show saturation %s
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Sat Sep 5 19:59:42 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 1.05/1.35 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.05/1.35
% 1.05/1.35 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 1.05/1.39
%------------------------------------------------------------------------------