%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN159-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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 : Tue Sep 29 02:06:54 PM UTC 2026
% Result : Unsatisfiable 0.21s 0.32s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 344
% Syntax : Number of formulae : 611 ( 59 unt; 0 def)
% Number of atoms : 1786 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 2228 (1053 ~;1175 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 43 ( 42 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 1053 (1053 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
s0(d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_1) ).
fof(f2,axiom,
q0(e,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_2) ).
fof(f3,axiom,
n0(d,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_3) ).
fof(f4,axiom,
m0(e,d,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_4) ).
fof(f5,axiom,
s0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_5) ).
fof(f6,axiom,
q0(b,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_6) ).
fof(f7,axiom,
n0(d,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_7) ).
fof(f8,axiom,
m0(e,d,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_8) ).
fof(f9,axiom,
r0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_9) ).
fof(f10,axiom,
p0(b,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_10) ).
fof(f11,axiom,
n0(e,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_11) ).
fof(f12,axiom,
! [X0] : m0(a,X0,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_12) ).
fof(f13,axiom,
r0(e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_13) ).
fof(f14,axiom,
! [X0] : p0(b,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_14) ).
fof(f15,axiom,
n0(a,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_15) ).
fof(f16,axiom,
m0(c,b,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_16) ).
fof(f17,axiom,
! [X0] : q0(X0,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_17) ).
fof(f18,axiom,
p0(c,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_18) ).
fof(f19,axiom,
! [X0,X1] : m0(X0,d,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_19) ).
fof(f20,axiom,
l0(a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_20) ).
fof(f21,axiom,
q0(b,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_21) ).
fof(f22,axiom,
p0(b,c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_22) ).
fof(f23,axiom,
m0(a,e,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_23) ).
fof(f24,axiom,
l0(c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_24) ).
fof(f25,axiom,
q0(d,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_25) ).
fof(f26,axiom,
n0(d,c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_26) ).
fof(f27,axiom,
m0(e,b,c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_27) ).
fof(f28,axiom,
k0(e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_28) ).
fof(f29,axiom,
q0(d,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_29) ).
fof(f30,axiom,
n0(e,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_30) ).
fof(f31,axiom,
m0(b,b,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_31) ).
fof(f32,axiom,
k0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_32) ).
fof(f33,axiom,
q0(d,c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_33) ).
fof(f34,axiom,
n0(c,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_34) ).
fof(f35,axiom,
m0(d,e,c),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_35) ).
fof(f36,axiom,
q0(a,b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_36) ).
fof(f37,axiom,
n0(b,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_37) ).
fof(f38,axiom,
m0(b,a,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_38) ).
fof(f39,axiom,
! [X0,X1] :
( k1(X0)
| ~ n0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_001) ).
fof(f40,axiom,
! [X0,X1] :
( l1(X0,X0)
| ~ n0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_002) ).
fof(f41,axiom,
! [X2,X3,X0,X1] :
( l1(X0,X1)
| ~ p0(X2,X0)
| ~ r0(X3)
| ~ m0(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_003) ).
fof(f42,axiom,
! [X0,X1] :
( l1(X0,X0)
| ~ k1(X0)
| ~ l0(X1)
| ~ l1(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_004) ).
fof(f43,axiom,
! [X0,X1] :
( m1(X0,X1,X0)
| ~ m0(X1,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_005) ).
fof(f44,axiom,
! [X0,X1] :
( m1(X0,X0,X0)
| ~ m0(X1,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_006) ).
fof(f45,axiom,
! [X2,X0,X1] :
( m1(X0,X1,X0)
| ~ p0(X2,X1)
| ~ r0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_007) ).
fof(f46,axiom,
( m1(b,b,b)
| ~ l0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_008) ).
fof(f47,axiom,
! [X2,X0,X1] :
( m1(X0,X0,X0)
| ~ s0(X1)
| ~ r0(X1)
| ~ q0(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_009) ).
fof(f48,axiom,
! [X0,X1] :
( m1(X0,X0,c)
| ~ n0(X1,X1)
| ~ l1(c,c)
| ~ p0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_010) ).
fof(f49,axiom,
! [X0,X1] :
( m1(X0,X0,X1)
| ~ k0(X0)
| ~ n0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_011) ).
fof(f50,axiom,
( m1(e,e,e)
| ~ r0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_012) ).
fof(f51,axiom,
! [X0,X1] :
( m1(X0,X0,X0)
| ~ q0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_013) ).
fof(f52,axiom,
! [X2,X0,X1] :
( m1(X0,X0,X0)
| ~ m0(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_014) ).
fof(f53,axiom,
! [X2,X0,X1] :
( m1(X0,X1,X1)
| ~ l0(X2)
| ~ m0(X1,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_015) ).
fof(f54,axiom,
! [X2,X3,X0,X1] :
( m1(X0,X1,X1)
| ~ m1(X2,X1,X0)
| ~ m1(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_016) ).
fof(f55,axiom,
! [X0,X1] :
( m1(X0,X0,X0)
| ~ s0(X0)
| ~ q0(X1,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_017) ).
fof(f56,axiom,
! [X2,X0,X1] :
( m1(X0,X0,X0)
| ~ q0(X1,X2)
| ~ q0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_018) ).
fof(f57,axiom,
! [X0,X1] :
( m1(X0,X1,c)
| ~ r0(c)
| ~ s0(d)
| ~ q0(X1,d)
| ~ p0(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_019) ).
fof(f58,axiom,
( m1(c,c,c)
| ~ l0(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_020) ).
fof(f59,axiom,
! [X0,X1] :
( m1(X0,X1,X0)
| ~ l0(X0)
| ~ k0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_021) ).
fof(f60,axiom,
( m1(e,e,e)
| ~ s0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_022) ).
fof(f61,axiom,
( m1(a,a,a)
| ~ l0(a)
| ~ s0(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_023) ).
fof(f62,axiom,
! [X2,X0,X1] :
( m1(X0,a,X1)
| ~ m0(a,X2,a)
| ~ q0(X0,X1)
| ~ m1(X1,c,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_024) ).
fof(f63,axiom,
! [X2,X0,X1] :
( m1(X0,X0,X0)
| ~ m0(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_025) ).
fof(f64,axiom,
! [X0,X1] :
( m1(X0,X0,X0)
| ~ l0(X0)
| ~ l0(X1)
| ~ p0(X1,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_026) ).
fof(f65,axiom,
( m1(b,b,b)
| ~ q0(c,d)
| ~ l1(a,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_027) ).
fof(f66,axiom,
! [X0] :
( m1(X0,X0,X0)
| ~ l0(X0)
| ~ k0(X0)
| ~ m0(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_028) ).
fof(f67,axiom,
! [X0,X1] :
( m1(X0,X1,X0)
| ~ p0(X0,X1)
| ~ s0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_029) ).
fof(f68,axiom,
( m1(e,e,e)
| ~ r0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_030) ).
fof(f69,axiom,
! [X0] :
( m1(c,a,c)
| ~ r0(e)
| ~ m0(a,e,c)
| ~ r0(X0)
| ~ k0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_031) ).
fof(f70,axiom,
! [X0] :
( m1(X0,X0,X0)
| ~ s0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_032) ).
fof(f71,axiom,
! [X2,X0,X1] :
( m1(X0,X0,X0)
| ~ q0(X1,X1)
| ~ m1(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_033) ).
fof(f72,axiom,
! [X0,X1] :
( m1(X0,X1,X1)
| ~ k1(a)
| ~ k1(X1)
| ~ q0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_034) ).
fof(f73,axiom,
! [X0,X1] :
( m1(X0,X1,X0)
| ~ r0(X0)
| ~ l0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_035) ).
fof(f74,axiom,
! [X0,X1] :
( n1(X0,X0,X1)
| ~ m0(b,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_036) ).
fof(f75,axiom,
! [X2,X0,X1] :
( n1(X0,X1,X0)
| ~ p0(X2,X0)
| ~ l0(X1)
| ~ r0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_037) ).
fof(f76,axiom,
! [X0] :
( n1(X0,X0,X0)
| ~ n0(X0,X0)
| ~ q0(a,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_038) ).
fof(f77,axiom,
! [X0,X1] :
( n1(X0,c,X0)
| ~ m0(X1,X0,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_039) ).
fof(f78,axiom,
! [X0,X1] :
( n1(X0,e,e)
| ~ m0(X0,X1,e)
| ~ k1(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_040) ).
fof(f79,axiom,
! [X0] :
( n1(e,e,X0)
| ~ s0(b)
| ~ m1(b,X0,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_041) ).
fof(f80,axiom,
! [X2,X3,X0,X1] :
( n1(X0,X0,X0)
| ~ m0(X1,X2,X1)
| ~ k0(X0)
| ~ q0(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_042) ).
fof(f81,axiom,
! [X0] :
( n1(X0,X0,X0)
| ~ k1(X0)
| ~ p0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_043) ).
fof(f82,axiom,
! [X2,X0,X1] :
( n1(X0,X1,X0)
| ~ p0(X0,X0)
| ~ p0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_044) ).
fof(f83,axiom,
( n1(d,d,d)
| ~ q0(d,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_045) ).
fof(f84,axiom,
! [X2,X0,X1] :
( n1(X0,X0,X0)
| ~ m1(X1,X2,X0)
| ~ k0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_046) ).
fof(f85,axiom,
! [X0,X1] :
( n1(X0,d,X1)
| ~ p0(X1,X1)
| ~ r0(X0)
| ~ l1(X1,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_047) ).
fof(f87,axiom,
( n1(c,c,c)
| ~ l0(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_049) ).
fof(f88,axiom,
! [X0,X1] :
( n1(X0,X1,X0)
| ~ s0(b)
| ~ l0(X0)
| ~ p0(b,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_050) ).
fof(f89,axiom,
! [X0,X1] :
( n1(X0,X0,X0)
| ~ m1(c,X0,X1)
| ~ m0(b,X1,c)
| ~ n1(X1,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_051) ).
fof(f90,axiom,
! [X2,X0,X1] :
( n1(X0,X0,X0)
| ~ m0(X1,X1,X1)
| ~ k1(X0)
| ~ s0(X0)
| ~ p0(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_052) ).
fof(f91,axiom,
! [X0] :
( n1(a,X0,b)
| ~ p0(X0,d)
| ~ p0(a,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_053) ).
fof(f92,axiom,
! [X2,X0,X1] :
( n1(X0,X1,X1)
| ~ l0(X2)
| ~ l1(X2,X0)
| ~ n1(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_054) ).
fof(f93,axiom,
( n1(d,e,e)
| ~ p0(d,d)
| ~ n1(e,e,e)
| ~ r0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_055) ).
fof(f94,axiom,
( n1(a,a,a)
| ~ l0(a)
| ~ r0(a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_056) ).
fof(f95,axiom,
! [X0] :
( n1(X0,X0,X0)
| ~ r0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_057) ).
fof(f96,axiom,
! [X0,X1] :
( n1(X0,X0,X0)
| ~ l1(X1,X0)
| ~ n0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_058) ).
fof(f97,axiom,
! [X2,X3,X0,X1] :
( n1(X0,X0,X1)
| ~ m0(X2,X3,X3)
| ~ m0(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_059) ).
fof(f98,axiom,
( n1(d,d,b)
| ~ q0(b,e)
| ~ m1(d,e,e)
| ~ k0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_060) ).
fof(f99,axiom,
! [X0] :
( n1(X0,X0,X0)
| ~ k0(X0)
| ~ s0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_061) ).
fof(f100,axiom,
! [X2,X0,X1] :
( n1(X0,X0,X0)
| ~ m0(X1,X1,X2)
| ~ n1(X1,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_062) ).
fof(f101,axiom,
! [X0,X1] :
( p1(X0,X0,X1)
| ~ n0(d,X0)
| ~ k0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_063) ).
fof(f102,axiom,
! [X2,X0,X1] :
( p1(X0,X0,X0)
| ~ m0(X1,X2,b)
| ~ l0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_064) ).
fof(f103,axiom,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ l1(X1,X1)
| ~ p0(X0,X1)
| ~ n0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_065) ).
fof(f104,axiom,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ n0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_066) ).
fof(f105,axiom,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ q0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_067) ).
fof(f106,axiom,
! [X0] :
( p1(X0,X0,X0)
| ~ k0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_068) ).
fof(f107,axiom,
! [X0,X1] :
( p1(X0,X0,X1)
| ~ p0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_069) ).
fof(f108,axiom,
( p1(c,c,c)
| ~ p0(a,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_070) ).
fof(f109,axiom,
! [X2,X3,X0,X1] :
( p1(X0,X1,X0)
| ~ l0(X2)
| ~ p1(X1,X3,X0)
| ~ s0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_071) ).
fof(f110,axiom,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ s0(X1)
| ~ s0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_072) ).
fof(f111,axiom,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ n0(e,b)
| ~ k0(b)
| ~ k0(X0)
| ~ k1(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_073) ).
fof(f112,axiom,
! [X0,X1] :
( p1(X0,X0,X1)
| ~ p0(X1,X0)
| ~ r0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_074) ).
fof(f113,axiom,
( p1(a,a,a)
| ~ p0(b,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_075) ).
fof(f115,axiom,
( p1(c,e,b)
| ~ m0(b,c,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_077) ).
fof(f116,axiom,
( p1(d,d,b)
| ~ p0(d,b)
| ~ m0(e,a,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_078) ).
fof(f117,axiom,
! [X0] :
( p1(X0,X0,X0)
| ~ k0(e)
| ~ k1(X0)
| ~ l0(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_079) ).
fof(f118,axiom,
! [X2,X3,X0,X1] :
( p1(X0,X0,X0)
| ~ n0(X1,X1)
| ~ l0(X2)
| ~ n1(X1,X3,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_080) ).
fof(f119,axiom,
! [X2,X3,X0,X1,X4] :
( p1(X0,X0,X0)
| ~ m1(X1,X2,X0)
| ~ q0(X2,X3)
| ~ l0(X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_081) ).
fof(f120,axiom,
! [X2,X3,X0,X1] :
( p1(X0,X1,X2)
| ~ m0(X2,X0,X3)
| ~ p1(X2,X0,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_082) ).
fof(f121,axiom,
! [X0,X1] :
( p1(X0,b,X1)
| ~ m1(X0,X1,b)
| ~ k0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_083) ).
fof(f122,axiom,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ m0(b,X1,b)
| ~ l1(X0,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_084) ).
fof(f123,axiom,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ p0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_085) ).
fof(f124,axiom,
! [X2,X0,X1] :
( p1(X0,X0,X0)
| ~ l0(X0)
| ~ m0(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_086) ).
fof(f125,axiom,
( p1(a,b,a)
| ~ r0(b)
| ~ p1(a,a,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_087) ).
fof(f126,axiom,
( p1(a,a,a)
| ~ l0(a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_088) ).
fof(f127,axiom,
! [X0] :
( p1(d,d,X0)
| ~ s0(X0)
| ~ n1(c,d,X0)
| ~ r0(d)
| ~ n0(c,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_089) ).
fof(f128,axiom,
( p1(e,e,e)
| ~ r0(e)
| ~ k0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_090) ).
fof(f129,axiom,
! [X2,X3,X0,X1,X4] :
( p1(X0,X0,X0)
| ~ q0(X1,X2)
| ~ k1(X3)
| ~ n1(X1,X0,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_091) ).
fof(f130,axiom,
! [X2,X3,X0,X1] :
( q1(X0,X1,X0)
| ~ n0(X2,X1)
| ~ p0(X3,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_092) ).
fof(f131,axiom,
! [X0,X1] :
( q1(X0,X0,X0)
| ~ q0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_093) ).
fof(f132,axiom,
( q1(b,e,e)
| ~ s0(e)
| ~ k0(b)
| ~ l0(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_094) ).
fof(f133,axiom,
! [X0,X1] :
( q1(X0,X1,X1)
| ~ p0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_095) ).
fof(f134,axiom,
! [X2,X3,X0,X1] :
( q1(X0,X0,X0)
| ~ n1(X1,X2,X2)
| ~ p0(X1,X3)
| ~ m1(X0,X2,X1)
| ~ q1(X3,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_096) ).
fof(f135,axiom,
! [X0] :
( q1(X0,X0,X0)
| ~ s0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_097) ).
fof(f136,axiom,
! [X2,X0,X1] :
( q1(X0,X0,X0)
| ~ s0(X0)
| ~ m0(X1,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_098) ).
fof(f137,axiom,
! [X2,X0,X1] :
( q1(X0,X1,X1)
| ~ k0(X2)
| ~ l0(X0)
| ~ q1(X1,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_099) ).
fof(f138,axiom,
! [X0,X1] :
( q1(X0,X0,X0)
| ~ n0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_100) ).
fof(f139,axiom,
! [X0] :
( q1(X0,X0,X0)
| ~ k1(X0)
| ~ q0(X0,b)
| ~ p1(b,b,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_101) ).
fof(f140,axiom,
! [X0,X1] :
( q1(X0,X0,X0)
| ~ k0(X0)
| ~ l0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_102) ).
fof(f141,axiom,
! [X0] :
( q1(X0,X0,X0)
| ~ m0(X0,c,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_103) ).
fof(f142,axiom,
! [X2,X3,X0,X1] :
( q1(X0,X1,X0)
| ~ l0(X0)
| ~ r0(X2)
| ~ p0(X3,X0)
| ~ q0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_104) ).
fof(f143,axiom,
! [X0,X1] :
( q1(X0,X0,X1)
| ~ s0(X0)
| ~ p0(X1,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_105) ).
fof(f144,axiom,
! [X0] :
( q1(X0,X0,X0)
| ~ s0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_106) ).
fof(f145,axiom,
! [X0] :
( q1(e,X0,X0)
| ~ m0(X0,d,X0)
| ~ m0(e,d,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_107) ).
fof(f146,axiom,
! [X2,X0,X1] :
( q1(X0,X0,X0)
| ~ p0(X1,X2)
| ~ p1(X0,b,b)
| ~ q0(b,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_108) ).
fof(f147,axiom,
! [X2,X0,X1] :
( q1(X0,X0,X1)
| ~ p0(X2,X2)
| ~ q0(X1,X0)
| ~ k1(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_109) ).
fof(f148,axiom,
! [X2,X0,X1] :
( q1(X0,X0,X0)
| ~ m0(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_110) ).
fof(f149,axiom,
( q1(d,d,c)
| ~ m0(c,b,a)
| ~ m1(c,d,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_111) ).
fof(f150,axiom,
! [X0] :
( q1(X0,X0,X0)
| ~ k1(X0)
| ~ s0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_112) ).
fof(f151,axiom,
! [X2,X0,X1] :
( q1(X0,X0,X1)
| ~ r0(X2)
| ~ m1(X0,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_113) ).
fof(f152,axiom,
! [X0,X1] :
( q1(X0,X0,X0)
| ~ m0(X0,X0,X1)
| ~ k0(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_114) ).
fof(f153,axiom,
( q1(b,b,b)
| ~ l0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_115) ).
fof(f154,axiom,
! [X0] :
( q1(X0,X0,X0)
| ~ r0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_116) ).
fof(f155,axiom,
( q1(d,d,d)
| ~ k0(e)
| ~ s0(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_117) ).
fof(f156,axiom,
! [X0,X1] :
( q1(X0,X0,X0)
| ~ p0(b,d)
| ~ s0(b)
| ~ n1(X1,d,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_118) ).
fof(f157,axiom,
! [X0] :
( q1(X0,b,b)
| ~ s0(X0)
| ~ s0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_119) ).
fof(f158,axiom,
( q1(b,b,b)
| ~ r0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_120) ).
fof(f159,axiom,
! [X2,X0,X1] :
( q1(X0,X0,X0)
| ~ m0(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_121) ).
fof(f160,axiom,
! [X0,X1] :
( q1(X0,X0,X0)
| ~ m0(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_122) ).
fof(f161,axiom,
! [X0] :
( q1(X0,X0,X0)
| ~ m0(c,X0,X0)
| ~ r0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_123) ).
fof(f162,axiom,
! [X0,X1] :
( r1(X0)
| ~ q0(X0,X1)
| ~ s0(d)
| ~ q1(d,X1,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_124) ).
fof(f163,axiom,
! [X0] :
( s1(X0)
| ~ p0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_125) ).
fof(f164,axiom,
! [X2,X0,X1] :
( s1(X0)
| ~ q0(X0,X1)
| ~ s1(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_126) ).
fof(f165,axiom,
! [X2,X3,X0,X1] :
( k2(X0,X1)
| ~ m1(X2,X1,X0)
| ~ k1(X3)
| ~ k2(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_127) ).
fof(f166,axiom,
! [X0] :
( k2(X0,X0)
| ~ n1(e,d,X0)
| ~ m1(X0,e,X0)
| ~ q1(X0,X0,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_128) ).
fof(f167,axiom,
! [X0,X1] :
( k2(X0,X0)
| ~ q1(X1,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_129) ).
fof(f168,axiom,
( k2(e,e)
| ~ l1(e,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_130) ).
fof(f169,axiom,
! [X0,X1] :
( l2(X0,X1)
| ~ s1(X0)
| ~ n0(e,X1)
| ~ l2(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_131) ).
fof(f171,axiom,
! [X2,X3,X0,X1] :
( l2(X0,X0)
| ~ p0(X1,X1)
| ~ s1(X2)
| ~ m0(X3,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_133) ).
fof(f172,axiom,
! [X2,X0,X1] :
( l2(X0,X0)
| ~ m0(X1,X0,X2)
| ~ m1(X2,X1,X1)
| ~ p0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_134) ).
fof(f173,axiom,
! [X2,X0,X1] :
( m2(X0)
| ~ s0(X0)
| ~ l1(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_135) ).
fof(f174,axiom,
( m2(b)
| ~ k1(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_136) ).
fof(f175,axiom,
! [X2,X0,X1] :
( n2(X0)
| ~ p1(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_137) ).
fof(f176,axiom,
( n2(a)
| ~ m1(b,a,e)
| ~ k1(c)
| ~ n1(e,a,e)
| ~ q1(c,a,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_138) ).
fof(f177,axiom,
( n2(c)
| ~ l1(e,c)
| ~ k0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_139) ).
fof(f178,axiom,
! [X0,X1] :
( n2(e)
| ~ r1(b)
| ~ r0(e)
| ~ p1(b,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_140) ).
fof(f179,axiom,
! [X0] :
( p2(X0,a,X0)
| ~ q1(X0,a,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_141) ).
fof(f180,axiom,
! [X0,X1] :
( p2(X0,X0,X0)
| ~ k1(X1)
| ~ k0(X1)
| ~ l2(a,X1)
| ~ k2(X0,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_142) ).
fof(f181,axiom,
( p2(c,e,e)
| ~ l1(c,b)
| ~ q1(e,e,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_143) ).
fof(f182,axiom,
! [X0] :
( p2(b,c,a)
| ~ r0(e)
| ~ n1(c,X0,X0)
| ~ p0(b,X0)
| ~ k2(c,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_144) ).
fof(f183,axiom,
! [X0,X1] :
( p2(e,X0,X1)
| ~ r0(e)
| ~ p1(X0,X1,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_145) ).
fof(f184,axiom,
! [X2,X3,X0,X1] :
( p2(X0,X1,X1)
| ~ p1(X0,X2,X3)
| ~ l1(X2,X3)
| ~ p2(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_146) ).
fof(f185,axiom,
( p2(e,c,c)
| ~ r1(d)
| ~ l1(e,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_147) ).
fof(f186,axiom,
! [X2,X0,X1] :
( p2(X0,X0,X0)
| ~ m1(X1,X2,X0)
| ~ p2(X1,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_148) ).
fof(f187,axiom,
! [X0,X1] :
( p2(X0,X0,d)
| ~ r1(a)
| ~ m0(X1,X0,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_149) ).
fof(f188,axiom,
! [X0,X1] :
( p2(X0,X0,X0)
| ~ m1(X1,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_150) ).
fof(f189,axiom,
( p2(d,d,d)
| ~ k1(d)
| ~ s0(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_151) ).
fof(f190,axiom,
! [X2,X0,X1] :
( p2(X0,X1,X1)
| ~ n1(X2,X1,X2)
| ~ p0(X0,X1)
| ~ p2(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_152) ).
fof(f191,axiom,
! [X0] :
( p2(X0,X0,X0)
| ~ n1(d,d,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_153) ).
fof(f192,axiom,
! [X0] :
( p2(X0,X0,X0)
| ~ q1(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_154) ).
fof(f193,axiom,
! [X2,X0,X1] :
( p2(X0,X1,X1)
| ~ k1(X2)
| ~ p2(e,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_155) ).
fof(f194,axiom,
! [X0,X1] :
( p2(X0,e,X1)
| ~ n1(e,X0,a)
| ~ q1(a,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_156) ).
fof(f195,axiom,
! [X0] :
( p2(X0,X0,X0)
| ~ l1(X0,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_157) ).
fof(f196,axiom,
! [X2,X0,X1] :
( p2(X0,X0,X1)
| ~ q1(c,X0,X2)
| ~ s1(c)
| ~ s0(e)
| ~ p2(X0,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_158) ).
fof(f197,axiom,
! [X0] :
( p2(X0,X0,X0)
| ~ k1(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_159) ).
fof(f198,axiom,
! [X2,X0,X1] :
( p2(X0,X0,X0)
| ~ m1(a,a,X1)
| ~ p2(a,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_160) ).
fof(f199,axiom,
( p2(d,b,b)
| ~ p1(d,b,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_161) ).
fof(f200,axiom,
! [X0] :
( p2(b,c,c)
| ~ p1(X0,b,b)
| ~ n1(e,e,X0)
| ~ q1(e,c,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_162) ).
fof(f201,axiom,
! [X0,X1] :
( p2(X0,X0,X0)
| ~ q1(X1,c,X1)
| ~ k2(X0,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_163) ).
fof(f202,axiom,
! [X2,X0,X1] :
( p2(X0,X0,X0)
| ~ p0(X0,X0)
| ~ r1(X1)
| ~ p2(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_164) ).
fof(f203,axiom,
! [X2,X0,X1] :
( p2(X0,X0,X0)
| ~ q1(X1,X2,X1)
| ~ p2(X1,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_165) ).
fof(f204,axiom,
! [X0] :
( p2(a,X0,d)
| ~ n0(X0,d)
| ~ m1(a,X0,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_166) ).
fof(f205,axiom,
! [X0] :
( p2(X0,X0,X0)
| ~ s1(X0)
| ~ k1(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_167) ).
fof(f206,axiom,
( p2(a,c,b)
| ~ l1(e,c)
| ~ l2(e,b)
| ~ r1(e)
| ~ m1(d,a,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_168) ).
fof(f207,axiom,
! [X2,X0,X1] :
( p2(X0,X0,X0)
| ~ q1(X1,X1,X1)
| ~ p1(X0,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_169) ).
fof(f208,axiom,
! [X0] :
( p2(X0,e,X0)
| ~ n1(X0,e,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_170) ).
fof(f209,axiom,
! [X0,X1] :
( p2(X0,X0,X0)
| ~ n1(X1,X1,X1)
| ~ p0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_171) ).
fof(f210,axiom,
( p2(a,a,a)
| ~ p1(e,e,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_172) ).
fof(f211,axiom,
! [X0,X1] :
( p2(X0,X0,X0)
| ~ r1(X1)
| ~ r0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_173) ).
fof(f212,axiom,
! [X0] :
( p2(X0,X0,X0)
| ~ n2(X0)
| ~ k1(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_174) ).
fof(f213,axiom,
! [X0,X1] :
( p2(X0,X0,X0)
| ~ l1(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_175) ).
fof(f214,axiom,
! [X0,X1] :
( p2(X0,X1,X0)
| ~ m1(X1,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_176) ).
fof(f215,axiom,
! [X0,X1] :
( q2(X0,X1,X1)
| ~ k0(X1)
| ~ p1(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_177) ).
fof(f216,axiom,
! [X2,X0,X1] :
( q2(X0,X0,X0)
| ~ q0(X1,X0)
| ~ n1(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_178) ).
fof(f217,axiom,
! [X0,X1] :
( q2(X0,X0,X0)
| ~ k1(X1)
| ~ n1(X0,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_179) ).
fof(f218,axiom,
( q2(d,a,a)
| ~ q2(d,c,a)
| ~ s1(c)
| ~ q0(e,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_180) ).
fof(f219,axiom,
! [X0] :
( q2(X0,X0,X0)
| ~ p1(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_181) ).
fof(f220,axiom,
! [X2,X0,X1] :
( q2(X0,X1,X0)
| ~ p1(X0,X0,X2)
| ~ n1(X1,X0,X2)
| ~ q2(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_182) ).
fof(f221,axiom,
! [X0,X1] :
( q2(X0,c,X1)
| ~ k1(X1)
| ~ l0(c)
| ~ l2(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_183) ).
fof(f222,axiom,
! [X0,X1] :
( q2(X0,X0,X0)
| ~ q1(X1,c,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_184) ).
fof(f223,axiom,
! [X2,X0,X1] :
( q2(X0,X0,X0)
| ~ n1(X1,d,X2)
| ~ k1(X0)
| ~ q2(X2,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_185) ).
fof(f224,axiom,
! [X0,X1] :
( q2(X0,X0,X1)
| ~ l1(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_186) ).
fof(f225,axiom,
! [X2,X3,X0,X1] :
( q2(X0,X1,X0)
| ~ r1(X1)
| ~ m0(X2,X3,X0)
| ~ k0(X1)
| ~ q2(X1,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_187) ).
fof(f226,axiom,
! [X0] :
( r2(X0)
| ~ r1(X0)
| ~ l0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_188) ).
fof(f227,axiom,
! [X0] :
( s2(X0)
| ~ q2(b,X0,b)
| ~ s1(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_189) ).
fof(f228,axiom,
( s2(d)
| ~ s1(a)
| ~ s0(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_190) ).
fof(f229,axiom,
( s2(d)
| ~ r1(d)
| ~ s1(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_191) ).
fof(f230,axiom,
! [X2,X3,X0,X1] :
( k3(X0,X1,X0)
| ~ s1(X1)
| ~ p2(X2,X1,X3)
| ~ n0(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_192) ).
fof(f231,axiom,
! [X0,X1] :
( k3(X0,X0,X0)
| ~ s1(X0)
| ~ q2(d,X1,d)
| ~ s2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_193) ).
fof(f232,axiom,
! [X0,X1] :
( k3(X0,X0,X1)
| ~ k2(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_194) ).
fof(f233,axiom,
( k3(c,c,c)
| ~ s2(e)
| ~ k2(c,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_195) ).
fof(f234,axiom,
! [X2,X0,X1] :
( k3(X0,X0,X0)
| ~ p2(X1,X2,X1)
| ~ m1(X0,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_196) ).
fof(f235,axiom,
! [X0,X1] :
( k3(X0,X0,X0)
| ~ l2(X1,b)
| ~ k1(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_197) ).
fof(f236,axiom,
( k3(c,c,c)
| ~ k0(a)
| ~ r2(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_198) ).
fof(f238,axiom,
! [X2,X0,X1] :
( k3(X0,X0,X0)
| ~ p2(X1,X2,e)
| ~ s1(X1)
| ~ k3(X0,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_200) ).
fof(f239,axiom,
! [X2,X3,X0,X1] :
( k3(X0,X0,X1)
| ~ p1(X1,X2,X0)
| ~ m2(X3)
| ~ m2(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_201) ).
fof(f240,axiom,
! [X2,X3,X0,X1,X4] :
( k3(X0,X0,X1)
| ~ q0(X2,X1)
| ~ k2(X0,X3)
| ~ k3(X1,X4,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_202) ).
fof(f241,axiom,
( k3(d,d,d)
| ~ p1(a,d,b)
| ~ r2(a)
| ~ l2(e,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_203) ).
fof(f242,axiom,
( k3(a,a,a)
| ~ r2(a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_204) ).
fof(f243,axiom,
! [X0,X1] :
( k3(X0,X0,X0)
| ~ p2(X1,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_205) ).
fof(f244,axiom,
! [X0,X1] :
( k3(X0,X1,X0)
| ~ p2(X1,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_206) ).
fof(f246,axiom,
! [X0] :
( k3(X0,X0,X0)
| ~ r2(c)
| ~ l1(b,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_208) ).
fof(f247,axiom,
! [X2,X3,X0,X1] :
( k3(X0,X0,X0)
| ~ m2(X1)
| ~ l1(X2,X3)
| ~ s2(X0)
| ~ k3(X2,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_209) ).
fof(f248,axiom,
! [X0] :
( k3(X0,X0,X0)
| ~ n2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_210) ).
fof(f249,axiom,
! [X0] :
( k3(X0,X0,X0)
| ~ l0(X0)
| ~ r2(e)
| ~ r0(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_211) ).
fof(f250,axiom,
! [X0] :
( k3(X0,X0,X0)
| ~ m2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_212) ).
fof(f251,axiom,
! [X2,X0,X1] :
( k3(X0,X0,X0)
| ~ r1(X0)
| ~ p2(X1,X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_213) ).
fof(f252,axiom,
( k3(c,c,c)
| ~ r2(c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_214) ).
fof(f253,axiom,
! [X0,X1] :
( l3(X0,X1)
| ~ r0(X0)
| ~ p2(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_215) ).
fof(f254,axiom,
! [X2,X0,X1] :
( l3(X0,X0)
| ~ p1(X0,X0,X1)
| ~ p2(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_216) ).
fof(f255,axiom,
! [X0] :
( l3(X0,X0)
| ~ n2(X0)
| ~ m2(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_217) ).
fof(f256,axiom,
! [X0] :
( l3(X0,X0)
| ~ r2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_218) ).
fof(f257,axiom,
! [X2,X0,X1] :
( l3(X0,X0)
| ~ n2(X1)
| ~ l1(X2,X0)
| ~ l3(X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_219) ).
fof(f258,axiom,
! [X0,X1] :
( l3(X0,X0)
| ~ s2(X1)
| ~ l1(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_220) ).
fof(f259,axiom,
( l3(d,d)
| ~ k2(a,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_221) ).
fof(f260,axiom,
! [X2,X0,X1] :
( l3(X0,X0)
| ~ k3(X1,X0,X0)
| ~ l2(X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_222) ).
fof(f261,axiom,
( l3(c,c)
| ~ k2(b,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_223) ).
fof(f262,axiom,
( l3(d,c)
| ~ s2(d)
| ~ k3(a,c,a)
| ~ r0(b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_224) ).
fof(f263,axiom,
! [X2,X3,X0,X1] :
( m3(X0,X1,X0)
| ~ m0(X2,X2,X1)
| ~ l2(X3,X0)
| ~ m0(X0,X3,X3)
| ~ s2(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_225) ).
fof(f264,axiom,
! [X2,X0,X1] :
( m3(X0,X0,X0)
| ~ k2(X1,X2)
| ~ m3(X0,X2,X0)
| ~ n0(X2,a)
| ~ l2(a,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_226) ).
fof(f265,axiom,
! [X2,X3,X0,X1] :
( m3(X0,X0,X0)
| ~ q0(X1,X2)
| ~ s0(X3)
| ~ s2(X2)
| ~ r2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_227) ).
fof(f266,axiom,
! [X2,X0,X1] :
( m3(X0,X1,X1)
| ~ n2(X0)
| ~ m2(X1)
| ~ m3(X2,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_228) ).
fof(f267,axiom,
( m3(b,b,b)
| ~ q2(a,b,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_229) ).
fof(f268,axiom,
( m3(c,b,d)
| ~ l1(d,b)
| ~ m2(d)
| ~ q2(b,c,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_230) ).
fof(f269,axiom,
! [X0,X1] :
( m3(X0,X1,X0)
| ~ r2(X0)
| ~ k2(c,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_231) ).
fof(f270,axiom,
! [X0] :
( m3(X0,X0,X0)
| ~ l2(X0,X0)
| ~ n2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_232) ).
fof(f271,axiom,
! [X0,X1] :
( m3(X0,X0,X0)
| ~ n2(X0)
| ~ m2(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_233) ).
fof(f272,axiom,
! [X0] :
( m3(X0,e,e)
| ~ n2(e)
| ~ p2(X0,e,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_234) ).
fof(f273,axiom,
! [X0,X1] :
( m3(X0,X0,X1)
| ~ r2(X1)
| ~ k3(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_235) ).
fof(f274,axiom,
! [X0] :
( m3(X0,X0,X0)
| ~ n2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_236) ).
fof(f275,axiom,
! [X0] :
( m3(X0,c,X0)
| ~ s2(c)
| ~ q2(X0,c,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_237) ).
fof(f276,axiom,
! [X0] :
( m3(X0,X0,X0)
| ~ p2(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_238) ).
fof(f277,axiom,
( m3(b,b,b)
| ~ l2(a,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_239) ).
fof(f278,axiom,
! [X2,X0,X1] :
( n3(X0)
| ~ p2(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_240) ).
fof(f279,axiom,
! [X2,X3,X0,X1] :
( p3(X0,X1,X2)
| ~ q2(X3,d,X0)
| ~ k2(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_241) ).
fof(f280,axiom,
! [X2,X0,X1] :
( p3(X0,X1,X2)
| ~ r2(X1)
| ~ k3(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_242) ).
fof(f281,axiom,
! [X0] :
( p3(X0,d,e)
| ~ l3(b,e)
| ~ p2(d,b,c)
| ~ n3(X0)
| ~ q2(X0,d,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_243) ).
fof(f282,axiom,
! [X0] :
( p3(X0,X0,X0)
| ~ n2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_244) ).
fof(f283,axiom,
! [X2,X0,X1] :
( p3(X0,X0,X0)
| ~ l1(X1,X1)
| ~ l3(X1,X0)
| ~ p3(X2,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_245) ).
fof(f284,axiom,
! [X0] :
( p3(X0,X0,X0)
| ~ l2(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_246) ).
fof(f285,axiom,
! [X2,X0,X1] :
( p3(X0,X0,X0)
| ~ n2(X0)
| ~ q2(X1,X2,X0)
| ~ s1(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_247) ).
fof(f286,axiom,
! [X0,X1] :
( p3(X0,X0,X0)
| ~ p2(X1,X0,X0)
| ~ n3(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_248) ).
fof(f287,axiom,
! [X0] :
( p3(X0,X0,X0)
| ~ k1(X0)
| ~ n2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_249) ).
fof(f288,axiom,
! [X2,X0,X1] :
( p3(X0,X0,X0)
| ~ k1(X0)
| ~ q2(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_250) ).
fof(f289,axiom,
! [X2,X3,X0,X1] :
( p3(X0,X1,X1)
| ~ m3(X1,X2,X3)
| ~ p2(X0,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_251) ).
fof(f290,axiom,
! [X2,X0,X1] :
( p3(X0,X0,X0)
| ~ q0(X1,X0)
| ~ k2(X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_252) ).
fof(f291,axiom,
( p3(b,c,b)
| ~ k2(c,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_253) ).
fof(f292,axiom,
! [X0] :
( p3(e,b,e)
| ~ m3(e,X0,e)
| ~ q2(X0,X0,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_254) ).
fof(f293,axiom,
! [X2,X0,X1] :
( q3(X0,X1)
| ~ q2(X2,X0,X1)
| ~ n0(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_255) ).
fof(f294,axiom,
! [X0,X1] :
( q3(X0,X0)
| ~ p2(X1,X0,X0)
| ~ q3(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_256) ).
fof(f295,axiom,
! [X2,X0,X1] :
( q3(X0,X1)
| ~ n1(X2,X0,X1)
| ~ s2(X0)
| ~ q3(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_257) ).
fof(f296,axiom,
! [X2,X0,X1] :
( q3(X0,X0)
| ~ r2(X0)
| ~ s1(X1)
| ~ l2(X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_258) ).
fof(f297,axiom,
! [X0,X1] :
( q3(X0,X0)
| ~ m0(X1,d,X1)
| ~ k1(X0)
| ~ r2(d)
| ~ q3(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_259) ).
fof(f298,axiom,
! [X0,X1] :
( r3(X0,X1,X1)
| ~ s2(X1)
| ~ l2(c,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_260) ).
fof(f299,axiom,
! [X2,X0,X1] :
( r3(X0,X0,X0)
| ~ l1(X1,X2)
| ~ n1(X2,X2,X2)
| ~ r2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_261) ).
fof(f300,axiom,
! [X2,X0,X1] :
( r3(X0,X0,X0)
| ~ p1(X1,X2,X0)
| ~ l2(X2,X1)
| ~ r3(X0,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_262) ).
fof(f301,axiom,
! [X0,X1] :
( r3(X0,X0,X0)
| ~ m0(d,X1,X0)
| ~ r3(X0,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_263) ).
fof(f302,axiom,
! [X0] :
( r3(X0,X0,X0)
| ~ s2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_264) ).
fof(f303,axiom,
! [X0,X1] :
( r3(X0,X0,X0)
| ~ l2(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_265) ).
fof(f304,axiom,
! [X0] :
( r3(X0,X0,X0)
| ~ r2(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_266) ).
fof(f305,axiom,
! [X2,X0,X1] :
( r3(X0,X1,X0)
| ~ p2(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_267) ).
fof(f306,axiom,
! [X2,X3,X0,X1] :
( r3(X0,X0,X1)
| ~ m2(X1)
| ~ m3(X2,b,X0)
| ~ r3(X1,X3,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_268) ).
fof(f307,axiom,
! [X0] :
( r3(a,a,e)
| ~ k2(a,a)
| ~ q2(X0,e,X0)
| ~ m2(b)
| ~ m3(a,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_269) ).
fof(f308,axiom,
! [X0] :
( r3(X0,b,X0)
| ~ r0(X0)
| ~ p2(b,X0,b)
| ~ l2(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_270) ).
fof(f309,axiom,
! [X2,X0,X1] :
( r3(X0,X0,X0)
| ~ p3(X1,X0,X2)
| ~ r3(X1,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_271) ).
fof(f310,axiom,
! [X2,X0,X1] :
( r3(X0,X1,X2)
| ~ k2(X1,X2)
| ~ r2(X2)
| ~ r3(X2,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_272) ).
fof(f311,axiom,
! [X2,X3,X0,X1] :
( s3(X0,X1)
| ~ q2(X2,X0,X2)
| ~ s2(X0)
| ~ m0(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_273) ).
fof(f312,axiom,
( k4(c)
| ~ n0(c,d)
| ~ q3(e,b)
| ~ n3(e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_274) ).
fof(f314,axiom,
! [X0,X1] :
( k4(e)
| ~ q3(X0,X0)
| ~ q1(a,a,X1)
| ~ r3(X0,e,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_276) ).
fof(f315,axiom,
! [X2,X0,X1] :
( l4(X0)
| ~ p3(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_277) ).
fof(f316,axiom,
! [X0,X1] :
( l4(X0)
| ~ m0(X1,X0,X0)
| ~ l4(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_278) ).
fof(f317,axiom,
! [X2,X0,X1] :
( m4(X0,X1)
| ~ l2(X2,X1)
| ~ s3(a,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_279) ).
fof(f319,axiom,
! [X0,X1] :
( n4(X0,X1)
| ~ p3(X0,X1,X1)
| ~ n4(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_281) ).
fof(f320,axiom,
( n4(d,d)
| ~ k3(c,c,e)
| ~ q1(d,d,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_282) ).
fof(f321,axiom,
( n4(e,e)
| ~ l3(b,a)
| ~ p3(b,e,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_283) ).
fof(f322,axiom,
! [X0,X1] :
( n4(X0,X0)
| ~ k4(X1)
| ~ m3(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_284) ).
fof(f323,axiom,
! [X0,X1] :
( p4(X0,X0,X1)
| ~ r0(X0)
| ~ r3(X1,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_285) ).
fof(f324,axiom,
! [X2,X0,X1] :
( p4(X0,X0,X0)
| ~ q3(X1,X2)
| ~ n3(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_286) ).
fof(f325,axiom,
! [X0,X1] :
( p4(X0,X1,X0)
| ~ k3(X0,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_287) ).
fof(f326,axiom,
! [X2,X3,X0,X1] :
( p4(X0,X1,X1)
| ~ r3(X1,X1,X0)
| ~ p4(X2,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_288) ).
fof(f327,axiom,
! [X2,X3,X0,X1] :
( p4(X0,X0,X0)
| ~ l4(X0)
| ~ n0(X0,X1)
| ~ p4(X2,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_289) ).
fof(f328,axiom,
! [X2,X0,X1] :
( p4(X0,X0,X0)
| ~ m3(X1,X2,X0)
| ~ p4(X0,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_290) ).
fof(f329,axiom,
! [X0,X1] :
( p4(X0,X0,X0)
| ~ p3(X1,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_291) ).
fof(f330,axiom,
! [X2,X0,X1] :
( p4(X0,X0,X0)
| ~ k3(X1,X2,X2)
| ~ n4(X0,X2)
| ~ p1(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_292) ).
fof(f331,axiom,
! [X2,X0,X1] :
( p4(X0,X0,X0)
| ~ q3(X1,X2)
| ~ n4(X2,X0)
| ~ l3(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_293) ).
fof(f332,axiom,
! [X0] :
( p4(c,c,X0)
| ~ n3(a)
| ~ m3(X0,c,a) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_294) ).
fof(f333,axiom,
! [X2,X3,X0,X1,X4] :
( q4(X0,X1)
| ~ k3(X2,X2,X0)
| ~ q2(X3,X1,X0)
| ~ m3(X3,X4,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_295) ).
fof(f334,axiom,
! [X2,X0,X1] :
( q4(X0,X0)
| ~ r1(X0)
| ~ l4(X1)
| ~ q4(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_296) ).
fof(f335,axiom,
( q4(b,b)
| ~ k3(c,e,b)
| ~ l1(b,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_297) ).
fof(f336,axiom,
! [X2,X3,X0,X1] :
( r4(X0)
| ~ n3(X0)
| ~ q3(X1,X2)
| ~ p0(X3,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_298) ).
fof(f337,axiom,
! [X2,X3,X0,X1] :
( s4(X0)
| ~ p3(X1,X2,X3)
| ~ l1(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_299) ).
fof(f338,axiom,
! [X2,X0,X1] :
( k5(X0)
| ~ s4(X1)
| ~ r3(X2,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_300) ).
fof(f339,axiom,
( k5(b)
| ~ s4(e)
| ~ n1(b,b,b) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_301) ).
fof(f345,axiom,
! [X2,X3,X0,X1,X4] :
( n5(X0,X1)
| ~ q4(X2,X3)
| ~ n4(X0,X3)
| ~ p4(X4,X4,X1)
| ~ n5(X4,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_307) ).
fof(f346,axiom,
! [X0,X1] :
( n5(X0,X0)
| ~ m0(X1,X0,X1)
| ~ n5(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_308) ).
fof(f347,axiom,
! [X0,X1] :
( n5(X0,X0)
| ~ n4(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_309) ).
fof(f348,axiom,
! [X2,X0,X1] :
( n5(X0,X0)
| ~ p0(X0,X1)
| ~ m4(X2,X2)
| ~ k5(d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_310) ).
fof(f349,axiom,
( n5(d,d)
| ~ p4(c,d,c) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_311) ).
fof(f350,axiom,
( n5(b,e)
| ~ r3(d,b,c)
| ~ n4(b,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_312) ).
fof(f351,axiom,
! [X0,X1] :
( n5(X0,X0)
| ~ q4(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_313) ).
fof(f352,axiom,
! [X0] :
( n5(X0,X0)
| ~ r4(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_314) ).
fof(f353,axiom,
! [X0] :
( n5(X0,X0)
| ~ s1(X0)
| ~ k4(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_315) ).
fof(f354,axiom,
! [X2,X0,X1] :
( n5(X0,X0)
| ~ p4(X1,X0,X0)
| ~ s1(X0)
| ~ p4(b,b,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_316) ).
fof(f355,axiom,
! [X0] :
( n5(d,X0)
| ~ k3(d,X0,a)
| ~ n4(X0,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_317) ).
fof(f369,negated_conjecture,
~ n5(a,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f370,plain,
~ q0(e,d),
inference(consistent_polarity_flipping,[],[f2]) ).
fof(f371,plain,
~ n0(d,e),
inference(consistent_polarity_flipping,[],[f3]) ).
fof(f372,plain,
~ q0(b,b),
inference(consistent_polarity_flipping,[],[f6]) ).
fof(f373,plain,
~ n0(d,b),
inference(consistent_polarity_flipping,[],[f7]) ).
fof(f374,plain,
~ r0(b),
inference(consistent_polarity_flipping,[],[f9]) ).
fof(f375,plain,
~ n0(e,b),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f376,plain,
~ r0(e),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f377,plain,
~ n0(a,b),
inference(consistent_polarity_flipping,[],[f15]) ).
fof(f378,plain,
! [X0] : ~ q0(X0,d),
inference(consistent_polarity_flipping,[],[f17]) ).
fof(f379,plain,
~ q0(b,e),
inference(consistent_polarity_flipping,[],[f21]) ).
fof(f380,plain,
~ q0(d,d),
inference(consistent_polarity_flipping,[],[f25]) ).
fof(f381,plain,
~ n0(d,c),
inference(consistent_polarity_flipping,[],[f26]) ).
fof(f382,plain,
~ q0(d,b),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f383,plain,
~ n0(e,e),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f384,plain,
~ q0(d,c),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f385,plain,
~ n0(c,d),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f386,plain,
~ q0(a,b),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f387,plain,
~ n0(b,a),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f388,plain,
! [X0,X1] :
( k1(X0)
| n0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f389,plain,
! [X0,X1] :
( l1(X0,X0)
| n0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f390,plain,
! [X2,X3,X0,X1] :
( l1(X0,X1)
| ~ p0(X2,X0)
| r0(X3)
| ~ m0(X1,X0,X2) ),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f391,plain,
! [X2,X0,X1] :
( m1(X0,X1,X0)
| ~ p0(X2,X1)
| r0(X0) ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f392,plain,
! [X2,X0,X1] :
( m1(X0,X0,X0)
| ~ s0(X1)
| r0(X1)
| q0(X2,X0) ),
inference(consistent_polarity_flipping,[],[f47]) ).
fof(f393,plain,
! [X0,X1] :
( m1(X0,X0,c)
| n0(X1,X1)
| ~ l1(c,c)
| ~ p0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f394,plain,
! [X0,X1] :
( m1(X0,X0,X1)
| ~ k0(X0)
| n0(X1,X1) ),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f395,plain,
( m1(e,e,e)
| r0(e) ),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f396,plain,
! [X0,X1] :
( m1(X0,X0,X0)
| q0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f51]) ).
fof(f397,plain,
! [X0,X1] :
( m1(X0,X0,X0)
| ~ s0(X0)
| q0(X1,d) ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f398,plain,
! [X2,X0,X1] :
( m1(X0,X0,X0)
| q0(X1,X2)
| q0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f399,plain,
! [X0,X1] :
( m1(X0,X1,c)
| r0(c)
| ~ s0(d)
| q0(X1,d)
| ~ p0(X0,X1) ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f400,plain,
! [X2,X0,X1] :
( m1(X0,a,X1)
| ~ m0(a,X2,a)
| q0(X0,X1)
| ~ m1(X1,c,X1) ),
inference(consistent_polarity_flipping,[],[f62]) ).
fof(f401,plain,
( m1(b,b,b)
| q0(c,d)
| ~ l1(a,b) ),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f402,plain,
( m1(e,e,e)
| r0(e) ),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f403,plain,
! [X0] :
( m1(c,a,c)
| r0(e)
| ~ m0(a,e,c)
| r0(X0)
| ~ k0(e) ),
inference(consistent_polarity_flipping,[],[f69]) ).
fof(f404,plain,
! [X2,X0,X1] :
( m1(X0,X0,X0)
| q0(X1,X1)
| ~ m1(X2,X1,X0) ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f405,plain,
! [X0,X1] :
( m1(X0,X1,X1)
| ~ k1(a)
| ~ k1(X1)
| q0(X0,X0) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f406,plain,
! [X0,X1] :
( m1(X0,X1,X0)
| r0(X0)
| ~ l0(X1) ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f407,plain,
! [X2,X0,X1] :
( n1(X0,X1,X0)
| ~ p0(X2,X0)
| ~ l0(X1)
| r0(X0) ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f408,plain,
! [X0] :
( n1(X0,X0,X0)
| n0(X0,X0)
| q0(a,X0) ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f409,plain,
! [X2,X3,X0,X1] :
( n1(X0,X0,X0)
| ~ m0(X1,X2,X1)
| ~ k0(X0)
| q0(X3,X2) ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f410,plain,
( n1(d,d,d)
| q0(d,d) ),
inference(consistent_polarity_flipping,[],[f83]) ).
fof(f411,plain,
! [X0,X1] :
( n1(X0,d,X1)
| ~ p0(X1,X1)
| r0(X0)
| ~ l1(X1,d) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f412,plain,
( n1(d,e,e)
| ~ p0(d,d)
| ~ n1(e,e,e)
| r0(b) ),
inference(consistent_polarity_flipping,[],[f93]) ).
fof(f413,plain,
( n1(a,a,a)
| ~ l0(a)
| r0(a) ),
inference(consistent_polarity_flipping,[],[f94]) ).
fof(f414,plain,
! [X0] :
( n1(X0,X0,X0)
| r0(X0) ),
inference(consistent_polarity_flipping,[],[f95]) ).
fof(f415,plain,
! [X0,X1] :
( n1(X0,X0,X0)
| ~ l1(X1,X0)
| n0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f416,plain,
( n1(d,d,b)
| q0(b,e)
| ~ m1(d,e,e)
| ~ k0(b) ),
inference(consistent_polarity_flipping,[],[f98]) ).
fof(f417,plain,
! [X0,X1] :
( p1(X0,X0,X1)
| n0(d,X0)
| ~ k0(X1) ),
inference(consistent_polarity_flipping,[],[f101]) ).
fof(f418,plain,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ l1(X1,X1)
| ~ p0(X0,X1)
| n0(X1,X1) ),
inference(consistent_polarity_flipping,[],[f103]) ).
fof(f419,plain,
! [X0,X1] :
( p1(X0,X0,X0)
| n0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f420,plain,
! [X0,X1] :
( p1(X0,X0,X0)
| q0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f421,plain,
! [X0,X1] :
( p1(X0,X0,X0)
| n0(e,b)
| ~ k0(b)
| ~ k0(X0)
| ~ k1(X1) ),
inference(consistent_polarity_flipping,[],[f111]) ).
fof(f422,plain,
! [X0,X1] :
( p1(X0,X0,X1)
| ~ p0(X1,X0)
| r0(X0) ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f423,plain,
! [X2,X3,X0,X1] :
( p1(X0,X0,X0)
| n0(X1,X1)
| ~ l0(X2)
| ~ n1(X1,X3,X0) ),
inference(consistent_polarity_flipping,[],[f118]) ).
fof(f424,plain,
! [X2,X3,X0,X1,X4] :
( p1(X0,X0,X0)
| ~ m1(X1,X2,X0)
| q0(X2,X3)
| ~ l0(X4) ),
inference(consistent_polarity_flipping,[],[f119]) ).
fof(f425,plain,
( p1(a,b,a)
| r0(b)
| ~ p1(a,a,a) ),
inference(consistent_polarity_flipping,[],[f125]) ).
fof(f426,plain,
! [X0] :
( p1(d,d,X0)
| ~ s0(X0)
| ~ n1(c,d,X0)
| r0(d)
| n0(c,X0) ),
inference(consistent_polarity_flipping,[],[f127]) ).
fof(f427,plain,
( p1(e,e,e)
| r0(e)
| ~ k0(e) ),
inference(consistent_polarity_flipping,[],[f128]) ).
fof(f428,plain,
! [X2,X3,X0,X1,X4] :
( p1(X0,X0,X0)
| q0(X1,X2)
| ~ k1(X3)
| ~ n1(X1,X0,X4) ),
inference(consistent_polarity_flipping,[],[f129]) ).
fof(f429,plain,
! [X2,X3,X0,X1] :
( ~ q1(X0,X1,X0)
| n0(X2,X1)
| ~ p0(X3,X0) ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f430,plain,
! [X0,X1] :
( ~ q1(X0,X0,X0)
| q0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f131]) ).
fof(f431,plain,
( ~ q1(b,e,e)
| ~ s0(e)
| ~ k0(b)
| ~ l0(c) ),
inference(consistent_polarity_flipping,[],[f132]) ).
fof(f432,plain,
! [X0,X1] :
( ~ q1(X0,X1,X1)
| ~ p0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f133]) ).
fof(f433,plain,
! [X2,X3,X0,X1] :
( ~ q1(X0,X0,X0)
| ~ n1(X1,X2,X2)
| ~ p0(X1,X3)
| ~ m1(X0,X2,X1)
| q1(X3,X1,X2) ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f434,plain,
! [X0] :
( ~ q1(X0,X0,X0)
| ~ s0(X0) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f435,plain,
! [X2,X0,X1] :
( ~ q1(X0,X0,X0)
| ~ s0(X0)
| ~ m0(X1,X1,X2) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f436,plain,
! [X2,X0,X1] :
( ~ q1(X0,X1,X1)
| ~ k0(X2)
| ~ l0(X0)
| q1(X1,X1,X2) ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f437,plain,
! [X0,X1] :
( ~ q1(X0,X0,X0)
| n0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f438,plain,
! [X0] :
( ~ q1(X0,X0,X0)
| ~ k1(X0)
| q0(X0,b)
| ~ p1(b,b,X0) ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f439,plain,
! [X0,X1] :
( ~ q1(X0,X0,X0)
| ~ k0(X0)
| ~ l0(X1) ),
inference(consistent_polarity_flipping,[],[f140]) ).
fof(f440,plain,
! [X0] :
( ~ q1(X0,X0,X0)
| ~ m0(X0,c,b) ),
inference(consistent_polarity_flipping,[],[f141]) ).
fof(f441,plain,
! [X2,X3,X0,X1] :
( ~ q1(X0,X1,X0)
| ~ l0(X0)
| r0(X2)
| ~ p0(X3,X0)
| q0(X1,X1) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f442,plain,
! [X0,X1] :
( ~ q1(X0,X0,X1)
| ~ s0(X0)
| ~ p0(X1,d) ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f443,plain,
! [X0] :
( ~ q1(X0,X0,X0)
| ~ s0(X0) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f444,plain,
! [X0] :
( ~ q1(e,X0,X0)
| ~ m0(X0,d,X0)
| ~ m0(e,d,X0) ),
inference(consistent_polarity_flipping,[],[f145]) ).
fof(f445,plain,
! [X2,X0,X1] :
( ~ q1(X0,X0,X0)
| ~ p0(X1,X2)
| ~ p1(X0,b,b)
| q0(b,b) ),
inference(consistent_polarity_flipping,[],[f146]) ).
fof(f446,plain,
! [X2,X0,X1] :
( ~ q1(X0,X0,X1)
| ~ p0(X2,X2)
| q0(X1,X0)
| ~ k1(X0) ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f447,plain,
! [X2,X0,X1] :
( ~ q1(X0,X0,X0)
| ~ m0(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f448,plain,
( ~ q1(d,d,c)
| ~ m0(c,b,a)
| ~ m1(c,d,a) ),
inference(consistent_polarity_flipping,[],[f149]) ).
fof(f449,plain,
! [X0] :
( ~ q1(X0,X0,X0)
| ~ k1(X0)
| ~ s0(b) ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f450,plain,
! [X2,X0,X1] :
( ~ q1(X0,X0,X1)
| r0(X2)
| ~ m1(X0,X1,X1) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f451,plain,
! [X0,X1] :
( ~ q1(X0,X0,X0)
| ~ m0(X0,X0,X1)
| ~ k0(X1) ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f452,plain,
( ~ q1(b,b,b)
| ~ l0(b) ),
inference(consistent_polarity_flipping,[],[f153]) ).
fof(f453,plain,
! [X0] :
( ~ q1(X0,X0,X0)
| r0(X0) ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f454,plain,
( ~ q1(d,d,d)
| ~ k0(e)
| ~ s0(d) ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f455,plain,
! [X0,X1] :
( ~ q1(X0,X0,X0)
| ~ p0(b,d)
| ~ s0(b)
| ~ n1(X1,d,X0) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f456,plain,
! [X0] :
( ~ q1(X0,b,b)
| ~ s0(X0)
| ~ s0(b) ),
inference(consistent_polarity_flipping,[],[f157]) ).
fof(f457,plain,
( ~ q1(b,b,b)
| r0(b) ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f458,plain,
! [X2,X0,X1] :
( ~ q1(X0,X0,X0)
| ~ m0(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f459,plain,
! [X0,X1] :
( ~ q1(X0,X0,X0)
| ~ m0(X0,X1,X0) ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f460,plain,
! [X0] :
( ~ q1(X0,X0,X0)
| ~ m0(c,X0,X0)
| r0(X0) ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f461,plain,
! [X0,X1] :
( ~ r1(X0)
| q0(X0,X1)
| ~ s0(d)
| q1(d,X1,d) ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f462,plain,
! [X0] :
( ~ s1(X0)
| ~ p0(X0,X0) ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f463,plain,
! [X2,X0,X1] :
( ~ s1(X0)
| q0(X0,X1)
| s1(X2) ),
inference(consistent_polarity_flipping,[],[f164]) ).
fof(f464,plain,
! [X2,X3,X0,X1] :
( ~ k2(X0,X1)
| ~ m1(X2,X1,X0)
| ~ k1(X3)
| k2(X3,X1) ),
inference(consistent_polarity_flipping,[],[f165]) ).
fof(f465,plain,
! [X0] :
( ~ k2(X0,X0)
| ~ n1(e,d,X0)
| ~ m1(X0,e,X0)
| q1(X0,X0,d) ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f466,plain,
! [X0,X1] :
( ~ k2(X0,X0)
| q1(X1,X0,X0) ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f467,plain,
( ~ k2(e,e)
| ~ l1(e,e) ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f468,plain,
! [X0,X1] :
( ~ l2(X0,X1)
| s1(X0)
| n0(e,X1)
| l2(X1,X1) ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f469,plain,
! [X2,X3,X0,X1] :
( ~ l2(X0,X0)
| ~ p0(X1,X1)
| s1(X2)
| ~ m0(X3,X2,X0) ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f470,plain,
! [X2,X0,X1] :
( ~ l2(X0,X0)
| ~ m0(X1,X0,X2)
| ~ m1(X2,X1,X1)
| ~ p0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f172]) ).
fof(f471,plain,
! [X2,X0,X1] :
( ~ m2(X0)
| ~ s0(X0)
| ~ l1(X1,X2) ),
inference(consistent_polarity_flipping,[],[f173]) ).
fof(f472,plain,
( ~ m2(b)
| ~ k1(b) ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f473,plain,
( n2(a)
| ~ m1(b,a,e)
| ~ k1(c)
| ~ n1(e,a,e)
| q1(c,a,d) ),
inference(consistent_polarity_flipping,[],[f176]) ).
fof(f474,plain,
! [X0,X1] :
( n2(e)
| r1(b)
| r0(e)
| ~ p1(b,X0,X1) ),
inference(consistent_polarity_flipping,[],[f178]) ).
fof(f475,plain,
! [X0] :
( ~ p2(X0,a,X0)
| q1(X0,a,X0) ),
inference(consistent_polarity_flipping,[],[f179]) ).
fof(f476,plain,
! [X0,X1] :
( ~ p2(X0,X0,X0)
| ~ k1(X1)
| ~ k0(X1)
| l2(a,X1)
| k2(X0,a) ),
inference(consistent_polarity_flipping,[],[f180]) ).
fof(f477,plain,
( ~ p2(c,e,e)
| ~ l1(c,b)
| q1(e,e,e) ),
inference(consistent_polarity_flipping,[],[f181]) ).
fof(f478,plain,
! [X0] :
( ~ p2(b,c,a)
| r0(e)
| ~ n1(c,X0,X0)
| ~ p0(b,X0)
| k2(c,a) ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f479,plain,
! [X0,X1] :
( ~ p2(e,X0,X1)
| r0(e)
| ~ p1(X0,X1,e) ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f480,plain,
! [X2,X3,X0,X1] :
( ~ p2(X0,X1,X1)
| ~ p1(X0,X2,X3)
| ~ l1(X2,X3)
| p2(X0,X1,X0) ),
inference(consistent_polarity_flipping,[],[f184]) ).
fof(f481,plain,
( ~ p2(e,c,c)
| r1(d)
| ~ l1(e,c) ),
inference(consistent_polarity_flipping,[],[f185]) ).
fof(f482,plain,
! [X2,X0,X1] :
( ~ p2(X0,X0,X0)
| ~ m1(X1,X2,X0)
| p2(X1,X0,X1) ),
inference(consistent_polarity_flipping,[],[f186]) ).
fof(f483,plain,
! [X0,X1] :
( ~ p2(X0,X0,d)
| r1(a)
| ~ m0(X1,X0,d) ),
inference(consistent_polarity_flipping,[],[f187]) ).
fof(f484,plain,
! [X0,X1] :
( ~ p2(X0,X0,X0)
| ~ m1(X1,X1,X0) ),
inference(consistent_polarity_flipping,[],[f188]) ).
fof(f485,plain,
( ~ p2(d,d,d)
| ~ k1(d)
| ~ s0(d) ),
inference(consistent_polarity_flipping,[],[f189]) ).
fof(f486,plain,
! [X2,X0,X1] :
( ~ p2(X0,X1,X1)
| ~ n1(X2,X1,X2)
| ~ p0(X0,X1)
| p2(X0,X1,X0) ),
inference(consistent_polarity_flipping,[],[f190]) ).
fof(f487,plain,
! [X0] :
( ~ p2(X0,X0,X0)
| ~ n1(d,d,X0) ),
inference(consistent_polarity_flipping,[],[f191]) ).
fof(f488,plain,
! [X0] :
( ~ p2(X0,X0,X0)
| q1(X0,X0,X0) ),
inference(consistent_polarity_flipping,[],[f192]) ).
fof(f489,plain,
! [X2,X0,X1] :
( ~ p2(X0,X1,X1)
| ~ k1(X2)
| p2(e,X0,X1) ),
inference(consistent_polarity_flipping,[],[f193]) ).
fof(f490,plain,
! [X0,X1] :
( ~ p2(X0,e,X1)
| ~ n1(e,X0,a)
| q1(a,X1,X0) ),
inference(consistent_polarity_flipping,[],[f194]) ).
fof(f491,plain,
! [X0] :
( ~ p2(X0,X0,X0)
| ~ l1(X0,d) ),
inference(consistent_polarity_flipping,[],[f195]) ).
fof(f492,plain,
! [X2,X0,X1] :
( ~ p2(X0,X0,X1)
| q1(c,X0,X2)
| s1(c)
| ~ s0(e)
| p2(X0,X2,X0) ),
inference(consistent_polarity_flipping,[],[f196]) ).
fof(f493,plain,
! [X0] :
( ~ p2(X0,X0,X0)
| ~ k1(X0) ),
inference(consistent_polarity_flipping,[],[f197]) ).
fof(f494,plain,
! [X2,X0,X1] :
( ~ p2(X0,X0,X0)
| ~ m1(a,a,X1)
| p2(a,X2,X0) ),
inference(consistent_polarity_flipping,[],[f198]) ).
fof(f495,plain,
( ~ p2(d,b,b)
| ~ p1(d,b,e) ),
inference(consistent_polarity_flipping,[],[f199]) ).
fof(f496,plain,
! [X0] :
( ~ p2(b,c,c)
| ~ p1(X0,b,b)
| ~ n1(e,e,X0)
| q1(e,c,X0) ),
inference(consistent_polarity_flipping,[],[f200]) ).
fof(f497,plain,
! [X0,X1] :
( ~ p2(X0,X0,X0)
| q1(X1,c,X1)
| k2(X0,c) ),
inference(consistent_polarity_flipping,[],[f201]) ).
fof(f498,plain,
! [X2,X0,X1] :
( ~ p2(X0,X0,X0)
| ~ p0(X0,X0)
| r1(X1)
| p2(X2,X1,X0) ),
inference(consistent_polarity_flipping,[],[f202]) ).
fof(f499,plain,
! [X2,X0,X1] :
( ~ p2(X0,X0,X0)
| q1(X1,X2,X1)
| p2(X1,X1,X2) ),
inference(consistent_polarity_flipping,[],[f203]) ).
fof(f500,plain,
! [X0] :
( ~ p2(a,X0,d)
| n0(X0,d)
| ~ m1(a,X0,d) ),
inference(consistent_polarity_flipping,[],[f204]) ).
fof(f501,plain,
! [X0] :
( ~ p2(X0,X0,X0)
| s1(X0)
| ~ k1(X0) ),
inference(consistent_polarity_flipping,[],[f205]) ).
fof(f502,plain,
( ~ p2(a,c,b)
| ~ l1(e,c)
| l2(e,b)
| r1(e)
| ~ m1(d,a,c) ),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f503,plain,
! [X2,X0,X1] :
( ~ p2(X0,X0,X0)
| q1(X1,X1,X1)
| ~ p1(X0,X2,X0) ),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f504,plain,
! [X0] :
( ~ p2(X0,e,X0)
| ~ n1(X0,e,e) ),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f505,plain,
! [X0,X1] :
( ~ p2(X0,X0,X0)
| ~ n1(X1,X1,X1)
| ~ p0(X0,X0) ),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f506,plain,
( ~ p2(a,a,a)
| ~ p1(e,e,a) ),
inference(consistent_polarity_flipping,[],[f210]) ).
fof(f507,plain,
! [X0,X1] :
( ~ p2(X0,X0,X0)
| r1(X1)
| r0(X0) ),
inference(consistent_polarity_flipping,[],[f211]) ).
fof(f508,plain,
! [X0] :
( ~ p2(X0,X0,X0)
| ~ n2(X0)
| ~ k1(e) ),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f509,plain,
! [X0,X1] :
( ~ p2(X0,X0,X0)
| ~ l1(X1,X0) ),
inference(consistent_polarity_flipping,[],[f213]) ).
fof(f510,plain,
! [X0,X1] :
( ~ p2(X0,X1,X0)
| ~ m1(X1,X0,X1) ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f511,plain,
! [X0,X1] :
( ~ q2(X0,X1,X1)
| ~ k0(X1)
| ~ p1(X0,X0,X0) ),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f512,plain,
! [X2,X0,X1] :
( ~ q2(X0,X0,X0)
| q0(X1,X0)
| ~ n1(X1,X0,X2) ),
inference(consistent_polarity_flipping,[],[f216]) ).
fof(f513,plain,
! [X0,X1] :
( ~ q2(X0,X0,X0)
| ~ k1(X1)
| ~ n1(X0,X0,X1) ),
inference(consistent_polarity_flipping,[],[f217]) ).
fof(f514,plain,
( ~ q2(d,a,a)
| q2(d,c,a)
| s1(c)
| q0(e,c) ),
inference(consistent_polarity_flipping,[],[f218]) ).
fof(f515,plain,
! [X0] :
( ~ q2(X0,X0,X0)
| ~ p1(X0,X0,X0) ),
inference(consistent_polarity_flipping,[],[f219]) ).
fof(f516,plain,
! [X2,X0,X1] :
( ~ q2(X0,X1,X0)
| ~ p1(X0,X0,X2)
| ~ n1(X1,X0,X2)
| q2(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f220]) ).
fof(f517,plain,
! [X0,X1] :
( ~ q2(X0,c,X1)
| ~ k1(X1)
| ~ l0(c)
| l2(X1,X0) ),
inference(consistent_polarity_flipping,[],[f221]) ).
fof(f518,plain,
! [X0,X1] :
( ~ q2(X0,X0,X0)
| q1(X1,c,X0) ),
inference(consistent_polarity_flipping,[],[f222]) ).
fof(f519,plain,
! [X2,X0,X1] :
( ~ q2(X0,X0,X0)
| ~ n1(X1,d,X2)
| ~ k1(X0)
| q2(X2,X2,X1) ),
inference(consistent_polarity_flipping,[],[f223]) ).
fof(f520,plain,
! [X0,X1] :
( ~ q2(X0,X0,X1)
| ~ l1(X1,X0) ),
inference(consistent_polarity_flipping,[],[f224]) ).
fof(f521,plain,
! [X2,X3,X0,X1] :
( ~ q2(X0,X1,X0)
| r1(X1)
| ~ m0(X2,X3,X0)
| ~ k0(X1)
| q2(X1,X1,X1) ),
inference(consistent_polarity_flipping,[],[f225]) ).
fof(f522,plain,
! [X0] :
( ~ r2(X0)
| r1(X0)
| ~ l0(X0) ),
inference(consistent_polarity_flipping,[],[f226]) ).
fof(f523,plain,
! [X0] :
( ~ s2(X0)
| q2(b,X0,b)
| s1(b) ),
inference(consistent_polarity_flipping,[],[f227]) ).
fof(f524,plain,
( ~ s2(d)
| s1(a)
| ~ s0(d) ),
inference(consistent_polarity_flipping,[],[f228]) ).
fof(f525,plain,
( ~ s2(d)
| r1(d)
| s1(d) ),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f526,plain,
! [X2,X3,X0,X1] :
( k3(X0,X1,X0)
| s1(X1)
| p2(X2,X1,X3)
| n0(X0,X3) ),
inference(consistent_polarity_flipping,[],[f230]) ).
fof(f527,plain,
! [X0,X1] :
( k3(X0,X0,X0)
| s1(X0)
| q2(d,X1,d)
| s2(X1) ),
inference(consistent_polarity_flipping,[],[f231]) ).
fof(f528,plain,
! [X0,X1] :
( k3(X0,X0,X1)
| k2(X1,X0) ),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f529,plain,
( k3(c,c,c)
| s2(e)
| k2(c,e) ),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f530,plain,
! [X2,X0,X1] :
( k3(X0,X0,X0)
| p2(X1,X2,X1)
| ~ m1(X0,X0,X2) ),
inference(consistent_polarity_flipping,[],[f234]) ).
fof(f531,plain,
! [X0,X1] :
( k3(X0,X0,X0)
| l2(X1,b)
| ~ k1(X0) ),
inference(consistent_polarity_flipping,[],[f235]) ).
fof(f532,plain,
( k3(c,c,c)
| ~ k0(a)
| r2(c) ),
inference(consistent_polarity_flipping,[],[f236]) ).
fof(f533,plain,
! [X2,X0,X1] :
( k3(X0,X0,X0)
| p2(X1,X2,e)
| s1(X1)
| ~ k3(X0,X1,X1) ),
inference(consistent_polarity_flipping,[],[f238]) ).
fof(f534,plain,
! [X2,X3,X0,X1] :
( k3(X0,X0,X1)
| ~ p1(X1,X2,X0)
| m2(X3)
| m2(X2) ),
inference(consistent_polarity_flipping,[],[f239]) ).
fof(f535,plain,
! [X2,X3,X0,X1,X4] :
( k3(X0,X0,X1)
| q0(X2,X1)
| k2(X0,X3)
| ~ k3(X1,X4,X3) ),
inference(consistent_polarity_flipping,[],[f240]) ).
fof(f536,plain,
( k3(d,d,d)
| ~ p1(a,d,b)
| r2(a)
| l2(e,b) ),
inference(consistent_polarity_flipping,[],[f241]) ).
fof(f537,plain,
( k3(a,a,a)
| r2(a) ),
inference(consistent_polarity_flipping,[],[f242]) ).
fof(f538,plain,
! [X0,X1] :
( k3(X0,X0,X0)
| p2(X1,X0,X0) ),
inference(consistent_polarity_flipping,[],[f243]) ).
fof(f539,plain,
! [X0,X1] :
( k3(X0,X1,X0)
| p2(X1,X0,X0) ),
inference(consistent_polarity_flipping,[],[f244]) ).
fof(f540,plain,
! [X0] :
( k3(X0,X0,X0)
| r2(c)
| ~ l1(b,X0) ),
inference(consistent_polarity_flipping,[],[f246]) ).
fof(f541,plain,
! [X2,X3,X0,X1] :
( k3(X0,X0,X0)
| m2(X1)
| ~ l1(X2,X3)
| s2(X0)
| ~ k3(X2,X3,X2) ),
inference(consistent_polarity_flipping,[],[f247]) ).
fof(f542,plain,
! [X0] :
( k3(X0,X0,X0)
| ~ l0(X0)
| r2(e)
| r0(e) ),
inference(consistent_polarity_flipping,[],[f249]) ).
fof(f543,plain,
! [X0] :
( k3(X0,X0,X0)
| m2(X0) ),
inference(consistent_polarity_flipping,[],[f250]) ).
fof(f544,plain,
! [X2,X0,X1] :
( k3(X0,X0,X0)
| r1(X0)
| p2(X1,X2,X2) ),
inference(consistent_polarity_flipping,[],[f251]) ).
fof(f545,plain,
( k3(c,c,c)
| r2(c) ),
inference(consistent_polarity_flipping,[],[f252]) ).
fof(f546,plain,
! [X0,X1] :
( ~ l3(X0,X1)
| r0(X0)
| p2(X0,X1,X0) ),
inference(consistent_polarity_flipping,[],[f253]) ).
fof(f547,plain,
! [X2,X0,X1] :
( ~ l3(X0,X0)
| ~ p1(X0,X0,X1)
| p2(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f254]) ).
fof(f548,plain,
! [X0] :
( ~ l3(X0,X0)
| ~ n2(X0)
| m2(b) ),
inference(consistent_polarity_flipping,[],[f255]) ).
fof(f549,plain,
! [X0] :
( ~ l3(X0,X0)
| r2(X0) ),
inference(consistent_polarity_flipping,[],[f256]) ).
fof(f550,plain,
! [X2,X0,X1] :
( ~ l3(X0,X0)
| ~ n2(X1)
| ~ l1(X2,X0)
| l3(X2,X2) ),
inference(consistent_polarity_flipping,[],[f257]) ).
fof(f551,plain,
! [X0,X1] :
( ~ l3(X0,X0)
| s2(X1)
| ~ l1(X0,X0) ),
inference(consistent_polarity_flipping,[],[f258]) ).
fof(f552,plain,
( ~ l3(d,d)
| k2(a,d) ),
inference(consistent_polarity_flipping,[],[f259]) ).
fof(f553,plain,
! [X2,X0,X1] :
( ~ l3(X0,X0)
| ~ k3(X1,X0,X0)
| l2(X2,X2) ),
inference(consistent_polarity_flipping,[],[f260]) ).
fof(f554,plain,
( ~ l3(c,c)
| k2(b,c) ),
inference(consistent_polarity_flipping,[],[f261]) ).
fof(f555,plain,
( ~ l3(d,c)
| s2(d)
| ~ k3(a,c,a)
| r0(b) ),
inference(consistent_polarity_flipping,[],[f262]) ).
fof(f556,plain,
! [X2,X3,X0,X1] :
( ~ m3(X0,X1,X0)
| ~ m0(X2,X2,X1)
| l2(X3,X0)
| ~ m0(X0,X3,X3)
| s2(X2) ),
inference(consistent_polarity_flipping,[],[f263]) ).
fof(f557,plain,
! [X2,X0,X1] :
( ~ m3(X0,X0,X0)
| k2(X1,X2)
| m3(X0,X2,X0)
| n0(X2,a)
| l2(a,a) ),
inference(consistent_polarity_flipping,[],[f264]) ).
fof(f558,plain,
! [X2,X3,X0,X1] :
( ~ m3(X0,X0,X0)
| q0(X1,X2)
| ~ s0(X3)
| s2(X2)
| r2(X0) ),
inference(consistent_polarity_flipping,[],[f265]) ).
fof(f559,plain,
! [X2,X0,X1] :
( ~ m3(X0,X1,X1)
| ~ n2(X0)
| m2(X1)
| m3(X2,X0,X2) ),
inference(consistent_polarity_flipping,[],[f266]) ).
fof(f560,plain,
( ~ m3(b,b,b)
| q2(a,b,a) ),
inference(consistent_polarity_flipping,[],[f267]) ).
fof(f561,plain,
( ~ m3(c,b,d)
| ~ l1(d,b)
| m2(d)
| q2(b,c,d) ),
inference(consistent_polarity_flipping,[],[f268]) ).
fof(f562,plain,
! [X0,X1] :
( ~ m3(X0,X1,X0)
| r2(X0)
| k2(c,X1) ),
inference(consistent_polarity_flipping,[],[f269]) ).
fof(f563,plain,
! [X0] :
( ~ m3(X0,X0,X0)
| l2(X0,X0)
| ~ n2(X0) ),
inference(consistent_polarity_flipping,[],[f270]) ).
fof(f564,plain,
! [X0,X1] :
( ~ m3(X0,X0,X0)
| ~ n2(X0)
| m2(X1) ),
inference(consistent_polarity_flipping,[],[f271]) ).
fof(f565,plain,
! [X0] :
( ~ m3(X0,e,e)
| ~ n2(e)
| p2(X0,e,e) ),
inference(consistent_polarity_flipping,[],[f272]) ).
fof(f566,plain,
! [X0,X1] :
( ~ m3(X0,X0,X1)
| r2(X1)
| ~ k3(X0,X1,X0) ),
inference(consistent_polarity_flipping,[],[f273]) ).
fof(f567,plain,
! [X0] :
( ~ m3(X0,X0,X0)
| ~ n2(X0) ),
inference(consistent_polarity_flipping,[],[f274]) ).
fof(f568,plain,
! [X0] :
( ~ m3(X0,c,X0)
| s2(c)
| q2(X0,c,c) ),
inference(consistent_polarity_flipping,[],[f275]) ).
fof(f569,plain,
! [X0] :
( ~ m3(X0,X0,X0)
| p2(X0,X0,X0) ),
inference(consistent_polarity_flipping,[],[f276]) ).
fof(f570,plain,
( ~ m3(b,b,b)
| l2(a,b) ),
inference(consistent_polarity_flipping,[],[f277]) ).
fof(f571,plain,
! [X2,X0,X1] :
( ~ n3(X0)
| p2(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f278]) ).
fof(f572,plain,
! [X2,X3,X0,X1] :
( p3(X0,X1,X2)
| q2(X3,d,X0)
| k2(X1,X2) ),
inference(consistent_polarity_flipping,[],[f279]) ).
fof(f573,plain,
! [X2,X0,X1] :
( p3(X0,X1,X2)
| r2(X1)
| ~ k3(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f280]) ).
fof(f574,plain,
! [X0] :
( p3(X0,d,e)
| l3(b,e)
| p2(d,b,c)
| n3(X0)
| q2(X0,d,X0) ),
inference(consistent_polarity_flipping,[],[f281]) ).
fof(f575,plain,
! [X2,X0,X1] :
( p3(X0,X0,X0)
| ~ l1(X1,X1)
| l3(X1,X0)
| ~ p3(X2,X2,X1) ),
inference(consistent_polarity_flipping,[],[f283]) ).
fof(f576,plain,
! [X0] :
( p3(X0,X0,X0)
| l2(X0,X0) ),
inference(consistent_polarity_flipping,[],[f284]) ).
fof(f577,plain,
! [X2,X0,X1] :
( p3(X0,X0,X0)
| ~ n2(X0)
| q2(X1,X2,X0)
| s1(X1) ),
inference(consistent_polarity_flipping,[],[f285]) ).
fof(f578,plain,
! [X0,X1] :
( p3(X0,X0,X0)
| p2(X1,X0,X0)
| n3(X0) ),
inference(consistent_polarity_flipping,[],[f286]) ).
fof(f579,plain,
! [X2,X0,X1] :
( p3(X0,X0,X0)
| ~ k1(X0)
| q2(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f288]) ).
fof(f580,plain,
! [X2,X3,X0,X1] :
( p3(X0,X1,X1)
| m3(X1,X2,X3)
| p2(X0,X1,X3) ),
inference(consistent_polarity_flipping,[],[f289]) ).
fof(f581,plain,
! [X2,X0,X1] :
( p3(X0,X0,X0)
| q0(X1,X0)
| k2(X2,X2) ),
inference(consistent_polarity_flipping,[],[f290]) ).
fof(f582,plain,
( p3(b,c,b)
| k2(c,b) ),
inference(consistent_polarity_flipping,[],[f291]) ).
fof(f583,plain,
! [X0] :
( p3(e,b,e)
| m3(e,X0,e)
| q2(X0,X0,b) ),
inference(consistent_polarity_flipping,[],[f292]) ).
fof(f584,plain,
! [X2,X0,X1] :
( ~ q3(X0,X1)
| q2(X2,X0,X1)
| n0(X2,X0) ),
inference(consistent_polarity_flipping,[],[f293]) ).
fof(f585,plain,
! [X0,X1] :
( ~ q3(X0,X0)
| p2(X1,X0,X0)
| q3(X1,X0) ),
inference(consistent_polarity_flipping,[],[f294]) ).
fof(f586,plain,
! [X2,X0,X1] :
( ~ q3(X0,X1)
| ~ n1(X2,X0,X1)
| s2(X0)
| q3(X1,X0) ),
inference(consistent_polarity_flipping,[],[f295]) ).
fof(f587,plain,
! [X2,X0,X1] :
( ~ q3(X0,X0)
| r2(X0)
| s1(X1)
| l2(X2,X2) ),
inference(consistent_polarity_flipping,[],[f296]) ).
fof(f588,plain,
! [X0,X1] :
( ~ q3(X0,X0)
| ~ m0(X1,d,X1)
| ~ k1(X0)
| r2(d)
| q3(X1,X0) ),
inference(consistent_polarity_flipping,[],[f297]) ).
fof(f589,plain,
! [X0,X1] :
( r3(X0,X1,X1)
| s2(X1)
| l2(c,X0) ),
inference(consistent_polarity_flipping,[],[f298]) ).
fof(f590,plain,
! [X2,X0,X1] :
( r3(X0,X0,X0)
| ~ l1(X1,X2)
| ~ n1(X2,X2,X2)
| r2(X0) ),
inference(consistent_polarity_flipping,[],[f299]) ).
fof(f591,plain,
! [X2,X0,X1] :
( r3(X0,X0,X0)
| ~ p1(X1,X2,X0)
| l2(X2,X1)
| ~ r3(X0,X1,X0) ),
inference(consistent_polarity_flipping,[],[f300]) ).
fof(f592,plain,
! [X0] :
( r3(X0,X0,X0)
| s2(X0) ),
inference(consistent_polarity_flipping,[],[f302]) ).
fof(f593,plain,
! [X0,X1] :
( r3(X0,X0,X0)
| l2(X1,X0) ),
inference(consistent_polarity_flipping,[],[f303]) ).
fof(f594,plain,
! [X0] :
( r3(X0,X0,X0)
| r2(X0) ),
inference(consistent_polarity_flipping,[],[f304]) ).
fof(f595,plain,
! [X2,X0,X1] :
( r3(X0,X1,X0)
| p2(X0,X2,X1) ),
inference(consistent_polarity_flipping,[],[f305]) ).
fof(f596,plain,
! [X2,X3,X0,X1] :
( r3(X0,X0,X1)
| m2(X1)
| m3(X2,b,X0)
| ~ r3(X1,X3,X3) ),
inference(consistent_polarity_flipping,[],[f306]) ).
fof(f597,plain,
! [X0] :
( r3(a,a,e)
| k2(a,a)
| q2(X0,e,X0)
| m2(b)
| m3(a,X0,X0) ),
inference(consistent_polarity_flipping,[],[f307]) ).
fof(f598,plain,
! [X0] :
( r3(X0,b,X0)
| r0(X0)
| p2(b,X0,b)
| l2(X0,X0) ),
inference(consistent_polarity_flipping,[],[f308]) ).
fof(f599,plain,
! [X2,X0,X1] :
( r3(X0,X1,X2)
| k2(X1,X2)
| r2(X2)
| ~ r3(X2,X0,X0) ),
inference(consistent_polarity_flipping,[],[f310]) ).
fof(f600,plain,
! [X2,X3,X0,X1] :
( s3(X0,X1)
| q2(X2,X0,X2)
| s2(X0)
| ~ m0(X2,X3,X1) ),
inference(consistent_polarity_flipping,[],[f311]) ).
fof(f601,plain,
( ~ k4(c)
| n0(c,d)
| q3(e,b)
| n3(e) ),
inference(consistent_polarity_flipping,[],[f312]) ).
fof(f602,plain,
! [X0,X1] :
( ~ k4(e)
| q3(X0,X0)
| q1(a,a,X1)
| ~ r3(X0,e,X1) ),
inference(consistent_polarity_flipping,[],[f314]) ).
fof(f603,plain,
! [X2,X0,X1] :
( ~ l4(X0)
| ~ p3(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f315]) ).
fof(f604,plain,
! [X0,X1] :
( ~ l4(X0)
| ~ m0(X1,X0,X0)
| l4(X1) ),
inference(consistent_polarity_flipping,[],[f316]) ).
fof(f605,plain,
! [X2,X0,X1] :
( m4(X0,X1)
| l2(X2,X1)
| ~ s3(a,X0) ),
inference(consistent_polarity_flipping,[],[f317]) ).
fof(f606,plain,
! [X0,X1] :
( ~ n4(X0,X1)
| ~ p3(X0,X1,X1)
| n4(X0,X0) ),
inference(consistent_polarity_flipping,[],[f319]) ).
fof(f607,plain,
( ~ n4(d,d)
| ~ k3(c,c,e)
| q1(d,d,d) ),
inference(consistent_polarity_flipping,[],[f320]) ).
fof(f608,plain,
( ~ n4(e,e)
| l3(b,a)
| ~ p3(b,e,a) ),
inference(consistent_polarity_flipping,[],[f321]) ).
fof(f609,plain,
! [X0,X1] :
( ~ n4(X0,X0)
| k4(X1)
| m3(X0,X0,X0) ),
inference(consistent_polarity_flipping,[],[f322]) ).
fof(f610,plain,
! [X0,X1] :
( p4(X0,X0,X1)
| r0(X0)
| ~ r3(X1,X0,X1) ),
inference(consistent_polarity_flipping,[],[f323]) ).
fof(f611,plain,
! [X2,X0,X1] :
( p4(X0,X0,X0)
| q3(X1,X2)
| n3(X0) ),
inference(consistent_polarity_flipping,[],[f324]) ).
fof(f612,plain,
! [X2,X3,X0,X1] :
( p4(X0,X0,X0)
| l4(X0)
| n0(X0,X1)
| ~ p4(X2,X3,X2) ),
inference(consistent_polarity_flipping,[],[f327]) ).
fof(f613,plain,
! [X2,X0,X1] :
( p4(X0,X0,X0)
| m3(X1,X2,X0)
| ~ p4(X0,X2,X0) ),
inference(consistent_polarity_flipping,[],[f328]) ).
fof(f614,plain,
! [X2,X0,X1] :
( p4(X0,X0,X0)
| ~ k3(X1,X2,X2)
| n4(X0,X2)
| ~ p1(X2,X1,X0) ),
inference(consistent_polarity_flipping,[],[f330]) ).
fof(f615,plain,
! [X2,X0,X1] :
( p4(X0,X0,X0)
| q3(X1,X2)
| n4(X2,X0)
| l3(X1,X1) ),
inference(consistent_polarity_flipping,[],[f331]) ).
fof(f616,plain,
! [X0] :
( p4(c,c,X0)
| n3(a)
| m3(X0,c,a) ),
inference(consistent_polarity_flipping,[],[f332]) ).
fof(f617,plain,
! [X2,X3,X0,X1,X4] :
( ~ q4(X0,X1)
| ~ k3(X2,X2,X0)
| q2(X3,X1,X0)
| m3(X3,X4,X3) ),
inference(consistent_polarity_flipping,[],[f333]) ).
fof(f618,plain,
! [X2,X0,X1] :
( ~ q4(X0,X0)
| r1(X0)
| l4(X1)
| q4(X1,X2) ),
inference(consistent_polarity_flipping,[],[f334]) ).
fof(f619,plain,
( ~ q4(b,b)
| ~ k3(c,e,b)
| ~ l1(b,c) ),
inference(consistent_polarity_flipping,[],[f335]) ).
fof(f620,plain,
! [X2,X3,X0,X1] :
( ~ r4(X0)
| n3(X0)
| q3(X1,X2)
| ~ p0(X3,X0) ),
inference(consistent_polarity_flipping,[],[f336]) ).
fof(f621,plain,
! [X2,X3,X0,X1] :
( ~ s4(X0)
| ~ p3(X1,X2,X3)
| ~ l1(X0,X2) ),
inference(consistent_polarity_flipping,[],[f337]) ).
fof(f622,plain,
! [X2,X0,X1] :
( k5(X0)
| s4(X1)
| ~ r3(X2,X0,X0) ),
inference(consistent_polarity_flipping,[],[f338]) ).
fof(f623,plain,
( k5(b)
| s4(e)
| ~ n1(b,b,b) ),
inference(consistent_polarity_flipping,[],[f339]) ).
fof(f624,plain,
! [X2,X3,X0,X1,X4] :
( ~ n5(X0,X1)
| q4(X2,X3)
| n4(X0,X3)
| ~ p4(X4,X4,X1)
| n5(X4,X1) ),
inference(consistent_polarity_flipping,[],[f345]) ).
fof(f625,plain,
! [X0,X1] :
( ~ n5(X0,X0)
| ~ m0(X1,X0,X1)
| n5(X1,X0) ),
inference(consistent_polarity_flipping,[],[f346]) ).
fof(f626,plain,
! [X0,X1] :
( ~ n5(X0,X0)
| n4(X1,X0) ),
inference(consistent_polarity_flipping,[],[f347]) ).
fof(f627,plain,
! [X2,X0,X1] :
( ~ n5(X0,X0)
| ~ p0(X0,X1)
| ~ m4(X2,X2)
| ~ k5(d) ),
inference(consistent_polarity_flipping,[],[f348]) ).
fof(f628,plain,
( ~ n5(d,d)
| ~ p4(c,d,c) ),
inference(consistent_polarity_flipping,[],[f349]) ).
fof(f629,plain,
( ~ n5(b,e)
| ~ r3(d,b,c)
| n4(b,e) ),
inference(consistent_polarity_flipping,[],[f350]) ).
fof(f630,plain,
! [X0,X1] :
( ~ n5(X0,X0)
| q4(X1,X0) ),
inference(consistent_polarity_flipping,[],[f351]) ).
fof(f631,plain,
! [X0] :
( ~ n5(X0,X0)
| r4(X0) ),
inference(consistent_polarity_flipping,[],[f352]) ).
fof(f632,plain,
! [X0] :
( ~ n5(X0,X0)
| s1(X0)
| k4(X0) ),
inference(consistent_polarity_flipping,[],[f353]) ).
fof(f633,plain,
! [X2,X0,X1] :
( ~ n5(X0,X0)
| ~ p4(X1,X0,X0)
| s1(X0)
| ~ p4(b,b,X2) ),
inference(consistent_polarity_flipping,[],[f354]) ).
fof(f634,plain,
! [X0] :
( ~ n5(d,X0)
| ~ k3(d,X0,a)
| n4(X0,d) ),
inference(consistent_polarity_flipping,[],[f355]) ).
fof(f635,plain,
n5(a,e),
inference(consistent_polarity_flipping,[],[f369]) ).
fof(f1643,plain,
$false,
inference(finite_model_not_found_(exhaustively_excluded_all_possible_domain_size_assignments),[],[f1,f370,f371,f4,f5,f372,f373,f8,f374,f10,f375,f12,f376,f14,f377,f16,f378,f18,f19,f20,f379,f22,f23,f24,f380,f381,f27,f28,f382,f383,f31,f32,f384,f385,f35,f386,f387,f38,f388,f389,f390,f42,f43,f44,f391,f46,f392,f393,f394,f395,f396,f52,f53,f54,f397,f398,f399,f58,f59,f60,f61,f400,f63,f64,f401,f66,f67,f402,f403,f70,f404,f405,f406,f74,f407,f408,f77,f78,f79,f409,f81,f82,f410,f84,f411,f87,f88,f89,f90,f91,f92,f412,f413,f414,f415,f97,f416,f99,f100,f417,f102,f418,f419,f420,f106,f107,f108,f109,f110,f421,f422,f113,f115,f116,f117,f423,f424,f120,f121,f122,f123,f124,f425,f126,f426,f427,f428,f429,f430,f431,f432,f433,f434,f435,f436,f437,f438,f439,f440,f441,f442,f443,f444,f445,f446,f447,f448,f449,f450,f451,f452,f453,f454,f455,f456,f457,f458,f459,f460,f461,f462,f463,f464,f465,f466,f467,f468,f469,f470,f471,f472,f175,f473,f177,f474,f475,f476,f477,f478,f479,f480,f481,f482,f483,f484,f485,f486,f487,f488,f489,f490,f491,f492,f493,f494,f495,f496,f497,f498,f499,f500,f501,f502,f503,f504,f505,f506,f507,f508,f509,f510,f511,f512,f513,f514,f515,f516,f517,f518,f519,f520,f521,f522,f523,f524,f525,f526,f527,f528,f529,f530,f531,f532,f533,f534,f535,f536,f537,f538,f539,f540,f541,f248,f542,f543,f544,f545,f546,f547,f548,f549,f550,f551,f552,f553,f554,f555,f556,f557,f558,f559,f560,f561,f562,f563,f564,f565,f566,f567,f568,f569,f570,f571,f572,f573,f574,f282,f575,f576,f577,f578,f287,f579,f580,f581,f582,f583,f584,f585,f586,f587,f588,f589,f590,f591,f301,f592,f593,f594,f595,f596,f597,f598,f309,f599,f600,f601,f602,f603,f604,f605,f606,f607,f608,f609,f610,f611,f325,f326,f612,f613,f329,f614,f615,f616,f617,f618,f619,f620,f621,f622,f623,f624,f625,f626,f627,f628,f629,f630,f631,f632,f633,f634,f635]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN159-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n003.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 15:39:13 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.32 % (1705682)Will run a generic schedule for satisfiability detection.
% 0.21/0.32 % (1705687)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=158555189_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.32 % (1705688)% WARNING: option uhcvi not known.
% 0.21/0.32 % (1705689)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3415330141:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.32 % (1705688)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=8775303:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.32 % (1705692)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1665534497:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.32 % (1705690)dis+10_1_sil=32000:sp=arity:random_seed=3340881723:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.32 % (1705691)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1515296865:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.32 % (1705693)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1398224082:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.32 % Detected minimum model sizes of [1]
% 0.21/0.32 % Detected maximum model sizes of [5]
% 0.21/0.32 % TRYING [1]
% 0.21/0.32 % TRYING [2]
% 0.21/0.32 % TRYING [3]
% 0.21/0.32 % TRYING [4]
% 0.21/0.32 % TRYING [5]
% 0.21/0.32 % (1705687) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1705682-1705687"...
% 0.21/0.32 % (1705687)...printing done.
% 0.21/0.32 % (1705687)Refutation found. Thanks to Tanya!
% 0.21/0.32 % SZS status Unsatisfiable for theBenchmark
% 0.21/0.32 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/0.32 % (1705687)------------------------------
% 0.21/0.32 % (1705687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.32 % (1705687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.32 % (1705687)CaDiCaL version: 2.1.3
% 0.21/0.32 % (1705687)Termination reason: Refutation
% 0.21/0.32 % (1705687)Time elapsed: 0.051 s
% 0.21/0.32 % (1705687)Peak memory usage: 17 MB
% 0.21/0.32 % (1705687)Instructions burned: 227 (million)
% 0.21/0.32 % (1705682)Success in time 0.088 s
% 0.21/0.32 % Vampire exiting
%------------------------------------------------------------------------------