%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM377+1.010 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.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 12:12:32 PM UTC 2026
% Result : Unsatisfiable 17.73s 3.54s
% Output : Refutation 18.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 326
% Syntax : Number of formulae : 983 ( 501 unt; 195 def)
% Number of atoms : 4951 (2480 equ)
% Maximal formula atoms : 250 ( 5 avg)
% Number of connectives : 7500 (3532 ~;3553 |; 220 &)
% ( 195 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 243 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 197 ( 195 usr; 196 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 33 con; 0-2 aty)
% Number of variables : 22 ( 0 sgn 0 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21] :
( succ(n0) = n1
& succ(n1) = n2
& succ(n2) = n3
& succ(n3) = n4
& succ(n4) = n5
& succ(n5) = n6
& succ(n6) = n7
& succ(n7) = n8
& succ(n8) = n9
& succ(n9) = n10
& succ(n10) = n0
& pred(n0) = n10
& pred(n1) = n0
& pred(n2) = n1
& pred(n3) = n2
& pred(n4) = n3
& pred(n5) = n4
& pred(n6) = n5
& pred(n7) = n6
& pred(n8) = n7
& pred(n9) = n8
& pred(n10) = n9
& sum(n0,n0) = n0
& sum(n0,n1) = n1
& sum(n0,n2) = n2
& sum(n0,n3) = n3
& sum(n0,n4) = n4
& sum(n0,n5) = n5
& sum(n0,n6) = n6
& sum(n0,n7) = n7
& sum(n0,n8) = n8
& sum(n0,n9) = n9
& sum(n0,n10) = n10
& sum(n1,n0) = n1
& sum(n1,n1) = n2
& sum(n1,n2) = n3
& sum(n1,n3) = n4
& sum(n1,n4) = n5
& sum(n1,n5) = n6
& sum(n1,n6) = n7
& sum(n1,n7) = n8
& sum(n1,n8) = n9
& sum(n1,n9) = n10
& sum(n1,n10) = n0
& sum(n2,n0) = n2
& sum(n2,n1) = n3
& sum(n2,n2) = n4
& sum(n2,n3) = n5
& sum(n2,n4) = n6
& sum(n2,n5) = n7
& sum(n2,n6) = n8
& sum(n2,n7) = n9
& sum(n2,n8) = n10
& sum(n2,n9) = n0
& sum(n2,n10) = n1
& sum(n3,n0) = n3
& sum(n3,n1) = n4
& sum(n3,n2) = n5
& sum(n3,n3) = n6
& sum(n3,n4) = n7
& sum(n3,n5) = n8
& sum(n3,n6) = n9
& sum(n3,n7) = n10
& sum(n3,n8) = n0
& sum(n3,n9) = n1
& sum(n3,n10) = n2
& sum(n4,n0) = n4
& sum(n4,n1) = n5
& sum(n4,n2) = n6
& sum(n4,n3) = n7
& sum(n4,n4) = n8
& sum(n4,n5) = n9
& sum(n4,n6) = n10
& sum(n4,n7) = n0
& sum(n4,n8) = n1
& sum(n4,n9) = n2
& sum(n4,n10) = n3
& sum(n5,n0) = n5
& sum(n5,n1) = n6
& sum(n5,n2) = n7
& sum(n5,n3) = n8
& sum(n5,n4) = n9
& sum(n5,n5) = n10
& sum(n5,n6) = n0
& sum(n5,n7) = n1
& sum(n5,n8) = n2
& sum(n5,n9) = n3
& sum(n5,n10) = n4
& sum(n6,n0) = n6
& sum(n6,n1) = n7
& sum(n6,n2) = n8
& sum(n6,n3) = n9
& sum(n6,n4) = n10
& sum(n6,n5) = n0
& sum(n6,n6) = n1
& sum(n6,n7) = n2
& sum(n6,n8) = n3
& sum(n6,n9) = n4
& sum(n6,n10) = n5
& sum(n7,n0) = n7
& sum(n7,n1) = n8
& sum(n7,n2) = n9
& sum(n7,n3) = n10
& sum(n7,n4) = n0
& sum(n7,n5) = n1
& sum(n7,n6) = n2
& sum(n7,n7) = n3
& sum(n7,n8) = n4
& sum(n7,n9) = n5
& sum(n7,n10) = n6
& sum(n8,n0) = n8
& sum(n8,n1) = n9
& sum(n8,n2) = n10
& sum(n8,n3) = n0
& sum(n8,n4) = n1
& sum(n8,n5) = n2
& sum(n8,n6) = n3
& sum(n8,n7) = n4
& sum(n8,n8) = n5
& sum(n8,n9) = n6
& sum(n8,n10) = n7
& sum(n9,n0) = n9
& sum(n9,n1) = n10
& sum(n9,n2) = n0
& sum(n9,n3) = n1
& sum(n9,n4) = n2
& sum(n9,n5) = n3
& sum(n9,n6) = n4
& sum(n9,n7) = n5
& sum(n9,n8) = n6
& sum(n9,n9) = n7
& sum(n9,n10) = n8
& sum(n10,n0) = n10
& sum(n10,n1) = n0
& sum(n10,n2) = n1
& sum(n10,n3) = n2
& sum(n10,n4) = n3
& sum(n10,n5) = n4
& sum(n10,n6) = n5
& sum(n10,n7) = n6
& sum(n10,n8) = n7
& sum(n10,n9) = n8
& sum(n10,n10) = n9
& ( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5
| X0 = n6
| X0 = n7
| X0 = n8
| X0 = n9
| X0 = n10 )
& ( X1 = n0
| X1 = n1
| X1 = n2
| X1 = n3
| X1 = n4
| X1 = n5
| X1 = n6
| X1 = n7
| X1 = n8
| X1 = n9
| X1 = n10 )
& X2 = sum(sum(pred(X0),succ(X1)),sum(pred(X1),succ(X0)))
& X3 = sum(sum(pred(X0),succ(X0)),sum(pred(X1),succ(X1)))
& X4 = sum(sum(pred(X2),succ(X3)),sum(pred(X3),succ(X2)))
& X5 = sum(sum(pred(X2),succ(X2)),sum(pred(X3),succ(X3)))
& X6 = sum(sum(pred(X4),succ(X5)),sum(pred(X5),succ(X4)))
& X7 = sum(sum(pred(X4),succ(X4)),sum(pred(X5),succ(X5)))
& X8 = sum(sum(pred(X6),succ(X7)),sum(pred(X7),succ(X6)))
& X9 = sum(sum(pred(X6),succ(X6)),sum(pred(X7),succ(X7)))
& X10 = sum(sum(pred(X8),succ(X9)),sum(pred(X9),succ(X8)))
& X11 = sum(sum(pred(X8),succ(X8)),sum(pred(X9),succ(X9)))
& X12 = sum(sum(pred(X10),succ(X11)),sum(pred(X11),succ(X10)))
& X13 = sum(sum(pred(X10),succ(X10)),sum(pred(X11),succ(X11)))
& X14 = sum(sum(pred(X12),succ(X13)),sum(pred(X13),succ(X12)))
& X15 = sum(sum(pred(X12),succ(X12)),sum(pred(X13),succ(X13)))
& X16 = sum(sum(pred(X14),succ(X15)),sum(pred(X15),succ(X14)))
& X17 = sum(sum(pred(X14),succ(X14)),sum(pred(X15),succ(X15)))
& X18 = sum(sum(pred(X16),succ(X17)),sum(pred(X17),succ(X16)))
& X19 = sum(sum(pred(X16),succ(X16)),sum(pred(X17),succ(X17)))
& X20 = sum(sum(pred(X18),succ(X19)),sum(pred(X19),succ(X18)))
& X21 = sum(sum(pred(X18),succ(X18)),sum(pred(X19),succ(X19)))
& ( X2 != X3
| X4 != X5
| X6 != X7
| X8 != X9
| X10 != X11
| X12 != X13
| X14 != X15
| X16 != X17
| X18 != X19
| X20 != X21 )
& n0 != n1
& n0 != n2
& n0 != n3
& n0 != n4
& n0 != n5
& n0 != n6
& n0 != n7
& n0 != n8
& n0 != n9
& n0 != n10
& n1 != n2
& n1 != n3
& n1 != n4
& n1 != n5
& n1 != n6
& n1 != n7
& n1 != n8
& n1 != n9
& n1 != n10
& n2 != n3
& n2 != n4
& n2 != n5
& n2 != n6
& n2 != n7
& n2 != n8
& n2 != n9
& n2 != n10
& n3 != n4
& n3 != n5
& n3 != n6
& n3 != n7
& n3 != n8
& n3 != n9
& n3 != n10
& n4 != n5
& n4 != n6
& n4 != n7
& n4 != n8
& n4 != n9
& n4 != n10
& n5 != n6
& n5 != n7
& n5 != n8
& n5 != n9
& n5 != n10
& n6 != n7
& n6 != n8
& n6 != n9
& n6 != n10
& n7 != n8
& n7 != n9
& n7 != n10
& n8 != n9
& n8 != n10
& n9 != n10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',try_satisfy_this) ).
fof(f2,plain,
( n10 = sK0
| n9 = sK0
| n8 = sK0
| n7 = sK0
| n6 = sK0
| n5 = sK0
| n4 = sK0
| n3 = sK0
| n2 = sK0
| n1 = sK0
| n0 = sK0 ),
inference(cnf_transformation,[],[f1]) ).
fof(f3,plain,
( n10 = sK1
| n9 = sK1
| n8 = sK1
| n7 = sK1
| n6 = sK1
| n5 = sK1
| n4 = sK1
| n3 = sK1
| n2 = sK1
| n1 = sK1
| n0 = sK1 ),
inference(cnf_transformation,[],[f1]) ).
fof(f4,plain,
( sK20 != sK21
| sK18 != sK19
| sK16 != sK17
| sK14 != sK15
| sK12 != sK13
| sK10 != sK11
| sK8 != sK9
| sK6 != sK7
| sK4 != sK5
| sK2 != sK3 ),
inference(cnf_transformation,[],[f1]) ).
fof(f60,plain,
sK21 = sum(sum(pred(sK18),succ(sK18)),sum(pred(sK19),succ(sK19))),
inference(cnf_transformation,[],[f1]) ).
fof(f61,plain,
sK20 = sum(sum(pred(sK18),succ(sK19)),sum(pred(sK19),succ(sK18))),
inference(cnf_transformation,[],[f1]) ).
fof(f62,plain,
sK19 = sum(sum(pred(sK16),succ(sK16)),sum(pred(sK17),succ(sK17))),
inference(cnf_transformation,[],[f1]) ).
fof(f63,plain,
sK18 = sum(sum(pred(sK16),succ(sK17)),sum(pred(sK17),succ(sK16))),
inference(cnf_transformation,[],[f1]) ).
fof(f64,plain,
sK17 = sum(sum(pred(sK14),succ(sK14)),sum(pred(sK15),succ(sK15))),
inference(cnf_transformation,[],[f1]) ).
fof(f65,plain,
sK16 = sum(sum(pred(sK14),succ(sK15)),sum(pred(sK15),succ(sK14))),
inference(cnf_transformation,[],[f1]) ).
fof(f66,plain,
sK15 = sum(sum(pred(sK12),succ(sK12)),sum(pred(sK13),succ(sK13))),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
sK14 = sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12))),
inference(cnf_transformation,[],[f1]) ).
fof(f68,plain,
sK13 = sum(sum(pred(sK10),succ(sK10)),sum(pred(sK11),succ(sK11))),
inference(cnf_transformation,[],[f1]) ).
fof(f69,plain,
sK12 = sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10))),
inference(cnf_transformation,[],[f1]) ).
fof(f70,plain,
sK11 = sum(sum(pred(sK8),succ(sK8)),sum(pred(sK9),succ(sK9))),
inference(cnf_transformation,[],[f1]) ).
fof(f71,plain,
sK10 = sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8))),
inference(cnf_transformation,[],[f1]) ).
fof(f72,plain,
sK9 = sum(sum(pred(sK6),succ(sK6)),sum(pred(sK7),succ(sK7))),
inference(cnf_transformation,[],[f1]) ).
fof(f73,plain,
sK8 = sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6))),
inference(cnf_transformation,[],[f1]) ).
fof(f74,plain,
sK7 = sum(sum(pred(sK4),succ(sK4)),sum(pred(sK5),succ(sK5))),
inference(cnf_transformation,[],[f1]) ).
fof(f75,plain,
sK6 = sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4))),
inference(cnf_transformation,[],[f1]) ).
fof(f76,plain,
sK5 = sum(sum(pred(sK2),succ(sK2)),sum(pred(sK3),succ(sK3))),
inference(cnf_transformation,[],[f1]) ).
fof(f77,plain,
sK4 = sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2))),
inference(cnf_transformation,[],[f1]) ).
fof(f78,plain,
sK3 = sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1))),
inference(cnf_transformation,[],[f1]) ).
fof(f79,plain,
sK2 = sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0))),
inference(cnf_transformation,[],[f1]) ).
fof(f80,plain,
n9 = sum(n10,n10),
inference(cnf_transformation,[],[f1]) ).
fof(f81,plain,
n8 = sum(n10,n9),
inference(cnf_transformation,[],[f1]) ).
fof(f82,plain,
n7 = sum(n10,n8),
inference(cnf_transformation,[],[f1]) ).
fof(f83,plain,
n6 = sum(n10,n7),
inference(cnf_transformation,[],[f1]) ).
fof(f84,plain,
n5 = sum(n10,n6),
inference(cnf_transformation,[],[f1]) ).
fof(f85,plain,
n4 = sum(n10,n5),
inference(cnf_transformation,[],[f1]) ).
fof(f86,plain,
n3 = sum(n10,n4),
inference(cnf_transformation,[],[f1]) ).
fof(f87,plain,
n2 = sum(n10,n3),
inference(cnf_transformation,[],[f1]) ).
fof(f88,plain,
n1 = sum(n10,n2),
inference(cnf_transformation,[],[f1]) ).
fof(f89,plain,
n0 = sum(n10,n1),
inference(cnf_transformation,[],[f1]) ).
fof(f90,plain,
n10 = sum(n10,n0),
inference(cnf_transformation,[],[f1]) ).
fof(f91,plain,
n8 = sum(n9,n10),
inference(cnf_transformation,[],[f1]) ).
fof(f92,plain,
n7 = sum(n9,n9),
inference(cnf_transformation,[],[f1]) ).
fof(f93,plain,
n6 = sum(n9,n8),
inference(cnf_transformation,[],[f1]) ).
fof(f94,plain,
n5 = sum(n9,n7),
inference(cnf_transformation,[],[f1]) ).
fof(f95,plain,
n4 = sum(n9,n6),
inference(cnf_transformation,[],[f1]) ).
fof(f96,plain,
n3 = sum(n9,n5),
inference(cnf_transformation,[],[f1]) ).
fof(f97,plain,
n2 = sum(n9,n4),
inference(cnf_transformation,[],[f1]) ).
fof(f98,plain,
n1 = sum(n9,n3),
inference(cnf_transformation,[],[f1]) ).
fof(f99,plain,
n0 = sum(n9,n2),
inference(cnf_transformation,[],[f1]) ).
fof(f100,plain,
n10 = sum(n9,n1),
inference(cnf_transformation,[],[f1]) ).
fof(f101,plain,
n9 = sum(n9,n0),
inference(cnf_transformation,[],[f1]) ).
fof(f102,plain,
n7 = sum(n8,n10),
inference(cnf_transformation,[],[f1]) ).
fof(f103,plain,
n6 = sum(n8,n9),
inference(cnf_transformation,[],[f1]) ).
fof(f104,plain,
n5 = sum(n8,n8),
inference(cnf_transformation,[],[f1]) ).
fof(f105,plain,
n4 = sum(n8,n7),
inference(cnf_transformation,[],[f1]) ).
fof(f106,plain,
n3 = sum(n8,n6),
inference(cnf_transformation,[],[f1]) ).
fof(f107,plain,
n2 = sum(n8,n5),
inference(cnf_transformation,[],[f1]) ).
fof(f108,plain,
n1 = sum(n8,n4),
inference(cnf_transformation,[],[f1]) ).
fof(f109,plain,
n0 = sum(n8,n3),
inference(cnf_transformation,[],[f1]) ).
fof(f110,plain,
n10 = sum(n8,n2),
inference(cnf_transformation,[],[f1]) ).
fof(f111,plain,
n9 = sum(n8,n1),
inference(cnf_transformation,[],[f1]) ).
fof(f112,plain,
n8 = sum(n8,n0),
inference(cnf_transformation,[],[f1]) ).
fof(f113,plain,
n6 = sum(n7,n10),
inference(cnf_transformation,[],[f1]) ).
fof(f114,plain,
n5 = sum(n7,n9),
inference(cnf_transformation,[],[f1]) ).
fof(f115,plain,
n4 = sum(n7,n8),
inference(cnf_transformation,[],[f1]) ).
fof(f116,plain,
n3 = sum(n7,n7),
inference(cnf_transformation,[],[f1]) ).
fof(f117,plain,
n2 = sum(n7,n6),
inference(cnf_transformation,[],[f1]) ).
fof(f118,plain,
n1 = sum(n7,n5),
inference(cnf_transformation,[],[f1]) ).
fof(f119,plain,
n0 = sum(n7,n4),
inference(cnf_transformation,[],[f1]) ).
fof(f120,plain,
n10 = sum(n7,n3),
inference(cnf_transformation,[],[f1]) ).
fof(f121,plain,
n9 = sum(n7,n2),
inference(cnf_transformation,[],[f1]) ).
fof(f122,plain,
n8 = sum(n7,n1),
inference(cnf_transformation,[],[f1]) ).
fof(f123,plain,
n7 = sum(n7,n0),
inference(cnf_transformation,[],[f1]) ).
fof(f124,plain,
n5 = sum(n6,n10),
inference(cnf_transformation,[],[f1]) ).
fof(f125,plain,
n4 = sum(n6,n9),
inference(cnf_transformation,[],[f1]) ).
fof(f126,plain,
n3 = sum(n6,n8),
inference(cnf_transformation,[],[f1]) ).
fof(f127,plain,
n2 = sum(n6,n7),
inference(cnf_transformation,[],[f1]) ).
fof(f128,plain,
n1 = sum(n6,n6),
inference(cnf_transformation,[],[f1]) ).
fof(f129,plain,
n0 = sum(n6,n5),
inference(cnf_transformation,[],[f1]) ).
fof(f130,plain,
n10 = sum(n6,n4),
inference(cnf_transformation,[],[f1]) ).
fof(f131,plain,
n9 = sum(n6,n3),
inference(cnf_transformation,[],[f1]) ).
fof(f132,plain,
n8 = sum(n6,n2),
inference(cnf_transformation,[],[f1]) ).
fof(f133,plain,
n7 = sum(n6,n1),
inference(cnf_transformation,[],[f1]) ).
fof(f134,plain,
n6 = sum(n6,n0),
inference(cnf_transformation,[],[f1]) ).
fof(f135,plain,
n4 = sum(n5,n10),
inference(cnf_transformation,[],[f1]) ).
fof(f136,plain,
n3 = sum(n5,n9),
inference(cnf_transformation,[],[f1]) ).
fof(f137,plain,
n2 = sum(n5,n8),
inference(cnf_transformation,[],[f1]) ).
fof(f138,plain,
n1 = sum(n5,n7),
inference(cnf_transformation,[],[f1]) ).
fof(f139,plain,
n0 = sum(n5,n6),
inference(cnf_transformation,[],[f1]) ).
fof(f140,plain,
n10 = sum(n5,n5),
inference(cnf_transformation,[],[f1]) ).
fof(f141,plain,
n9 = sum(n5,n4),
inference(cnf_transformation,[],[f1]) ).
fof(f142,plain,
n8 = sum(n5,n3),
inference(cnf_transformation,[],[f1]) ).
fof(f143,plain,
n7 = sum(n5,n2),
inference(cnf_transformation,[],[f1]) ).
fof(f144,plain,
n6 = sum(n5,n1),
inference(cnf_transformation,[],[f1]) ).
fof(f145,plain,
n5 = sum(n5,n0),
inference(cnf_transformation,[],[f1]) ).
fof(f146,plain,
n3 = sum(n4,n10),
inference(cnf_transformation,[],[f1]) ).
fof(f147,plain,
n2 = sum(n4,n9),
inference(cnf_transformation,[],[f1]) ).
fof(f148,plain,
n1 = sum(n4,n8),
inference(cnf_transformation,[],[f1]) ).
fof(f149,plain,
n0 = sum(n4,n7),
inference(cnf_transformation,[],[f1]) ).
fof(f150,plain,
n10 = sum(n4,n6),
inference(cnf_transformation,[],[f1]) ).
fof(f151,plain,
n9 = sum(n4,n5),
inference(cnf_transformation,[],[f1]) ).
fof(f152,plain,
n8 = sum(n4,n4),
inference(cnf_transformation,[],[f1]) ).
fof(f153,plain,
n7 = sum(n4,n3),
inference(cnf_transformation,[],[f1]) ).
fof(f154,plain,
n6 = sum(n4,n2),
inference(cnf_transformation,[],[f1]) ).
fof(f155,plain,
n5 = sum(n4,n1),
inference(cnf_transformation,[],[f1]) ).
fof(f156,plain,
n4 = sum(n4,n0),
inference(cnf_transformation,[],[f1]) ).
fof(f157,plain,
n2 = sum(n3,n10),
inference(cnf_transformation,[],[f1]) ).
fof(f158,plain,
n1 = sum(n3,n9),
inference(cnf_transformation,[],[f1]) ).
fof(f159,plain,
n0 = sum(n3,n8),
inference(cnf_transformation,[],[f1]) ).
fof(f160,plain,
n10 = sum(n3,n7),
inference(cnf_transformation,[],[f1]) ).
fof(f161,plain,
n9 = sum(n3,n6),
inference(cnf_transformation,[],[f1]) ).
fof(f162,plain,
n8 = sum(n3,n5),
inference(cnf_transformation,[],[f1]) ).
fof(f163,plain,
n7 = sum(n3,n4),
inference(cnf_transformation,[],[f1]) ).
fof(f164,plain,
n6 = sum(n3,n3),
inference(cnf_transformation,[],[f1]) ).
fof(f165,plain,
n5 = sum(n3,n2),
inference(cnf_transformation,[],[f1]) ).
fof(f166,plain,
n4 = sum(n3,n1),
inference(cnf_transformation,[],[f1]) ).
fof(f167,plain,
n3 = sum(n3,n0),
inference(cnf_transformation,[],[f1]) ).
fof(f168,plain,
n1 = sum(n2,n10),
inference(cnf_transformation,[],[f1]) ).
fof(f169,plain,
n0 = sum(n2,n9),
inference(cnf_transformation,[],[f1]) ).
fof(f170,plain,
n10 = sum(n2,n8),
inference(cnf_transformation,[],[f1]) ).
fof(f171,plain,
n9 = sum(n2,n7),
inference(cnf_transformation,[],[f1]) ).
fof(f172,plain,
n8 = sum(n2,n6),
inference(cnf_transformation,[],[f1]) ).
fof(f173,plain,
n7 = sum(n2,n5),
inference(cnf_transformation,[],[f1]) ).
fof(f174,plain,
n6 = sum(n2,n4),
inference(cnf_transformation,[],[f1]) ).
fof(f175,plain,
n5 = sum(n2,n3),
inference(cnf_transformation,[],[f1]) ).
fof(f176,plain,
n4 = sum(n2,n2),
inference(cnf_transformation,[],[f1]) ).
fof(f177,plain,
n3 = sum(n2,n1),
inference(cnf_transformation,[],[f1]) ).
fof(f178,plain,
n2 = sum(n2,n0),
inference(cnf_transformation,[],[f1]) ).
fof(f179,plain,
n0 = sum(n1,n10),
inference(cnf_transformation,[],[f1]) ).
fof(f180,plain,
n10 = sum(n1,n9),
inference(cnf_transformation,[],[f1]) ).
fof(f181,plain,
n9 = sum(n1,n8),
inference(cnf_transformation,[],[f1]) ).
fof(f182,plain,
n8 = sum(n1,n7),
inference(cnf_transformation,[],[f1]) ).
fof(f183,plain,
n7 = sum(n1,n6),
inference(cnf_transformation,[],[f1]) ).
fof(f184,plain,
n6 = sum(n1,n5),
inference(cnf_transformation,[],[f1]) ).
fof(f185,plain,
n5 = sum(n1,n4),
inference(cnf_transformation,[],[f1]) ).
fof(f186,plain,
n4 = sum(n1,n3),
inference(cnf_transformation,[],[f1]) ).
fof(f187,plain,
n3 = sum(n1,n2),
inference(cnf_transformation,[],[f1]) ).
fof(f188,plain,
n2 = sum(n1,n1),
inference(cnf_transformation,[],[f1]) ).
fof(f189,plain,
n1 = sum(n1,n0),
inference(cnf_transformation,[],[f1]) ).
fof(f190,plain,
n10 = sum(n0,n10),
inference(cnf_transformation,[],[f1]) ).
fof(f191,plain,
n9 = sum(n0,n9),
inference(cnf_transformation,[],[f1]) ).
fof(f192,plain,
n8 = sum(n0,n8),
inference(cnf_transformation,[],[f1]) ).
fof(f193,plain,
n7 = sum(n0,n7),
inference(cnf_transformation,[],[f1]) ).
fof(f194,plain,
n6 = sum(n0,n6),
inference(cnf_transformation,[],[f1]) ).
fof(f195,plain,
n5 = sum(n0,n5),
inference(cnf_transformation,[],[f1]) ).
fof(f196,plain,
n4 = sum(n0,n4),
inference(cnf_transformation,[],[f1]) ).
fof(f197,plain,
n3 = sum(n0,n3),
inference(cnf_transformation,[],[f1]) ).
fof(f198,plain,
n2 = sum(n0,n2),
inference(cnf_transformation,[],[f1]) ).
fof(f199,plain,
n1 = sum(n0,n1),
inference(cnf_transformation,[],[f1]) ).
fof(f200,plain,
n0 = sum(n0,n0),
inference(cnf_transformation,[],[f1]) ).
fof(f201,plain,
n9 = pred(n10),
inference(cnf_transformation,[],[f1]) ).
fof(f202,plain,
n8 = pred(n9),
inference(cnf_transformation,[],[f1]) ).
fof(f203,plain,
n7 = pred(n8),
inference(cnf_transformation,[],[f1]) ).
fof(f204,plain,
n6 = pred(n7),
inference(cnf_transformation,[],[f1]) ).
fof(f205,plain,
n5 = pred(n6),
inference(cnf_transformation,[],[f1]) ).
fof(f206,plain,
n4 = pred(n5),
inference(cnf_transformation,[],[f1]) ).
fof(f207,plain,
n3 = pred(n4),
inference(cnf_transformation,[],[f1]) ).
fof(f208,plain,
n2 = pred(n3),
inference(cnf_transformation,[],[f1]) ).
fof(f209,plain,
n1 = pred(n2),
inference(cnf_transformation,[],[f1]) ).
fof(f210,plain,
n0 = pred(n1),
inference(cnf_transformation,[],[f1]) ).
fof(f211,plain,
n10 = pred(n0),
inference(cnf_transformation,[],[f1]) ).
fof(f212,plain,
n0 = succ(n10),
inference(cnf_transformation,[],[f1]) ).
fof(f213,plain,
succ(n9) = n10,
inference(cnf_transformation,[],[f1]) ).
fof(f214,plain,
succ(n8) = n9,
inference(cnf_transformation,[],[f1]) ).
fof(f215,plain,
succ(n7) = n8,
inference(cnf_transformation,[],[f1]) ).
fof(f216,plain,
succ(n6) = n7,
inference(cnf_transformation,[],[f1]) ).
fof(f217,plain,
succ(n5) = n6,
inference(cnf_transformation,[],[f1]) ).
fof(f218,plain,
succ(n4) = n5,
inference(cnf_transformation,[],[f1]) ).
fof(f219,plain,
succ(n3) = n4,
inference(cnf_transformation,[],[f1]) ).
fof(f220,plain,
succ(n2) = n3,
inference(cnf_transformation,[],[f1]) ).
fof(f221,plain,
succ(n1) = n2,
inference(cnf_transformation,[],[f1]) ).
fof(f222,plain,
succ(n0) = n1,
inference(cnf_transformation,[],[f1]) ).
fof(f499,definition,
( spl22_56
<=> n9 = pred(n10) ),
introduced(definition,[new_symbols(definition,[spl22_56])],[avatar_definition]) ).
fof(f502,plain,
spl22_56,
inference(avatar_split_clause,[],[f201,f499]) ).
fof(f504,definition,
( spl22_57
<=> n8 = pred(n9) ),
introduced(definition,[new_symbols(definition,[spl22_57])],[avatar_definition]) ).
fof(f507,plain,
spl22_57,
inference(avatar_split_clause,[],[f202,f504]) ).
fof(f509,definition,
( spl22_58
<=> n7 = pred(n8) ),
introduced(definition,[new_symbols(definition,[spl22_58])],[avatar_definition]) ).
fof(f512,plain,
spl22_58,
inference(avatar_split_clause,[],[f203,f509]) ).
fof(f514,definition,
( spl22_59
<=> n6 = pred(n7) ),
introduced(definition,[new_symbols(definition,[spl22_59])],[avatar_definition]) ).
fof(f517,plain,
spl22_59,
inference(avatar_split_clause,[],[f204,f514]) ).
fof(f519,definition,
( spl22_60
<=> n5 = pred(n6) ),
introduced(definition,[new_symbols(definition,[spl22_60])],[avatar_definition]) ).
fof(f522,plain,
spl22_60,
inference(avatar_split_clause,[],[f205,f519]) ).
fof(f524,definition,
( spl22_61
<=> n4 = pred(n5) ),
introduced(definition,[new_symbols(definition,[spl22_61])],[avatar_definition]) ).
fof(f527,plain,
spl22_61,
inference(avatar_split_clause,[],[f206,f524]) ).
fof(f529,definition,
( spl22_62
<=> n3 = pred(n4) ),
introduced(definition,[new_symbols(definition,[spl22_62])],[avatar_definition]) ).
fof(f532,plain,
spl22_62,
inference(avatar_split_clause,[],[f207,f529]) ).
fof(f534,definition,
( spl22_63
<=> n2 = pred(n3) ),
introduced(definition,[new_symbols(definition,[spl22_63])],[avatar_definition]) ).
fof(f537,plain,
spl22_63,
inference(avatar_split_clause,[],[f208,f534]) ).
fof(f539,definition,
( spl22_64
<=> n1 = pred(n2) ),
introduced(definition,[new_symbols(definition,[spl22_64])],[avatar_definition]) ).
fof(f542,plain,
spl22_64,
inference(avatar_split_clause,[],[f209,f539]) ).
fof(f544,definition,
( spl22_65
<=> n0 = pred(n1) ),
introduced(definition,[new_symbols(definition,[spl22_65])],[avatar_definition]) ).
fof(f547,plain,
spl22_65,
inference(avatar_split_clause,[],[f210,f544]) ).
fof(f549,definition,
( spl22_66
<=> n10 = pred(n0) ),
introduced(definition,[new_symbols(definition,[spl22_66])],[avatar_definition]) ).
fof(f552,plain,
spl22_66,
inference(avatar_split_clause,[],[f211,f549]) ).
fof(f554,definition,
( spl22_67
<=> n0 = succ(n10) ),
introduced(definition,[new_symbols(definition,[spl22_67])],[avatar_definition]) ).
fof(f557,plain,
spl22_67,
inference(avatar_split_clause,[],[f212,f554]) ).
fof(f559,definition,
( spl22_68
<=> succ(n9) = n10 ),
introduced(definition,[new_symbols(definition,[spl22_68])],[avatar_definition]) ).
fof(f562,plain,
spl22_68,
inference(avatar_split_clause,[],[f213,f559]) ).
fof(f564,definition,
( spl22_69
<=> succ(n8) = n9 ),
introduced(definition,[new_symbols(definition,[spl22_69])],[avatar_definition]) ).
fof(f567,plain,
spl22_69,
inference(avatar_split_clause,[],[f214,f564]) ).
fof(f569,definition,
( spl22_70
<=> succ(n7) = n8 ),
introduced(definition,[new_symbols(definition,[spl22_70])],[avatar_definition]) ).
fof(f572,plain,
spl22_70,
inference(avatar_split_clause,[],[f215,f569]) ).
fof(f574,definition,
( spl22_71
<=> succ(n6) = n7 ),
introduced(definition,[new_symbols(definition,[spl22_71])],[avatar_definition]) ).
fof(f577,plain,
spl22_71,
inference(avatar_split_clause,[],[f216,f574]) ).
fof(f579,definition,
( spl22_72
<=> succ(n5) = n6 ),
introduced(definition,[new_symbols(definition,[spl22_72])],[avatar_definition]) ).
fof(f582,plain,
spl22_72,
inference(avatar_split_clause,[],[f217,f579]) ).
fof(f584,definition,
( spl22_73
<=> succ(n4) = n5 ),
introduced(definition,[new_symbols(definition,[spl22_73])],[avatar_definition]) ).
fof(f587,plain,
spl22_73,
inference(avatar_split_clause,[],[f218,f584]) ).
fof(f589,definition,
( spl22_74
<=> succ(n3) = n4 ),
introduced(definition,[new_symbols(definition,[spl22_74])],[avatar_definition]) ).
fof(f592,plain,
spl22_74,
inference(avatar_split_clause,[],[f219,f589]) ).
fof(f594,definition,
( spl22_75
<=> succ(n2) = n3 ),
introduced(definition,[new_symbols(definition,[spl22_75])],[avatar_definition]) ).
fof(f597,plain,
spl22_75,
inference(avatar_split_clause,[],[f220,f594]) ).
fof(f599,definition,
( spl22_76
<=> succ(n1) = n2 ),
introduced(definition,[new_symbols(definition,[spl22_76])],[avatar_definition]) ).
fof(f602,plain,
spl22_76,
inference(avatar_split_clause,[],[f221,f599]) ).
fof(f604,definition,
( spl22_77
<=> succ(n0) = n1 ),
introduced(definition,[new_symbols(definition,[spl22_77])],[avatar_definition]) ).
fof(f607,plain,
spl22_77,
inference(avatar_split_clause,[],[f222,f604]) ).
fof(f609,definition,
( spl22_78
<=> n9 = sum(n10,n10) ),
introduced(definition,[new_symbols(definition,[spl22_78])],[avatar_definition]) ).
fof(f612,plain,
spl22_78,
inference(avatar_split_clause,[],[f80,f609]) ).
fof(f614,definition,
( spl22_79
<=> n8 = sum(n10,n9) ),
introduced(definition,[new_symbols(definition,[spl22_79])],[avatar_definition]) ).
fof(f617,plain,
spl22_79,
inference(avatar_split_clause,[],[f81,f614]) ).
fof(f619,definition,
( spl22_80
<=> n7 = sum(n10,n8) ),
introduced(definition,[new_symbols(definition,[spl22_80])],[avatar_definition]) ).
fof(f622,plain,
spl22_80,
inference(avatar_split_clause,[],[f82,f619]) ).
fof(f624,definition,
( spl22_81
<=> n6 = sum(n10,n7) ),
introduced(definition,[new_symbols(definition,[spl22_81])],[avatar_definition]) ).
fof(f627,plain,
spl22_81,
inference(avatar_split_clause,[],[f83,f624]) ).
fof(f629,definition,
( spl22_82
<=> n5 = sum(n10,n6) ),
introduced(definition,[new_symbols(definition,[spl22_82])],[avatar_definition]) ).
fof(f632,plain,
spl22_82,
inference(avatar_split_clause,[],[f84,f629]) ).
fof(f634,definition,
( spl22_83
<=> n4 = sum(n10,n5) ),
introduced(definition,[new_symbols(definition,[spl22_83])],[avatar_definition]) ).
fof(f637,plain,
spl22_83,
inference(avatar_split_clause,[],[f85,f634]) ).
fof(f639,definition,
( spl22_84
<=> n3 = sum(n10,n4) ),
introduced(definition,[new_symbols(definition,[spl22_84])],[avatar_definition]) ).
fof(f642,plain,
spl22_84,
inference(avatar_split_clause,[],[f86,f639]) ).
fof(f644,definition,
( spl22_85
<=> n2 = sum(n10,n3) ),
introduced(definition,[new_symbols(definition,[spl22_85])],[avatar_definition]) ).
fof(f647,plain,
spl22_85,
inference(avatar_split_clause,[],[f87,f644]) ).
fof(f649,definition,
( spl22_86
<=> n1 = sum(n10,n2) ),
introduced(definition,[new_symbols(definition,[spl22_86])],[avatar_definition]) ).
fof(f652,plain,
spl22_86,
inference(avatar_split_clause,[],[f88,f649]) ).
fof(f654,definition,
( spl22_87
<=> n0 = sum(n10,n1) ),
introduced(definition,[new_symbols(definition,[spl22_87])],[avatar_definition]) ).
fof(f657,plain,
spl22_87,
inference(avatar_split_clause,[],[f89,f654]) ).
fof(f659,definition,
( spl22_88
<=> n10 = sum(n10,n0) ),
introduced(definition,[new_symbols(definition,[spl22_88])],[avatar_definition]) ).
fof(f662,plain,
spl22_88,
inference(avatar_split_clause,[],[f90,f659]) ).
fof(f664,definition,
( spl22_89
<=> n8 = sum(n9,n10) ),
introduced(definition,[new_symbols(definition,[spl22_89])],[avatar_definition]) ).
fof(f667,plain,
spl22_89,
inference(avatar_split_clause,[],[f91,f664]) ).
fof(f669,definition,
( spl22_90
<=> n7 = sum(n9,n9) ),
introduced(definition,[new_symbols(definition,[spl22_90])],[avatar_definition]) ).
fof(f672,plain,
spl22_90,
inference(avatar_split_clause,[],[f92,f669]) ).
fof(f674,definition,
( spl22_91
<=> n6 = sum(n9,n8) ),
introduced(definition,[new_symbols(definition,[spl22_91])],[avatar_definition]) ).
fof(f677,plain,
spl22_91,
inference(avatar_split_clause,[],[f93,f674]) ).
fof(f679,definition,
( spl22_92
<=> n5 = sum(n9,n7) ),
introduced(definition,[new_symbols(definition,[spl22_92])],[avatar_definition]) ).
fof(f682,plain,
spl22_92,
inference(avatar_split_clause,[],[f94,f679]) ).
fof(f684,definition,
( spl22_93
<=> n4 = sum(n9,n6) ),
introduced(definition,[new_symbols(definition,[spl22_93])],[avatar_definition]) ).
fof(f687,plain,
spl22_93,
inference(avatar_split_clause,[],[f95,f684]) ).
fof(f689,definition,
( spl22_94
<=> n3 = sum(n9,n5) ),
introduced(definition,[new_symbols(definition,[spl22_94])],[avatar_definition]) ).
fof(f692,plain,
spl22_94,
inference(avatar_split_clause,[],[f96,f689]) ).
fof(f694,definition,
( spl22_95
<=> n2 = sum(n9,n4) ),
introduced(definition,[new_symbols(definition,[spl22_95])],[avatar_definition]) ).
fof(f697,plain,
spl22_95,
inference(avatar_split_clause,[],[f97,f694]) ).
fof(f699,definition,
( spl22_96
<=> n1 = sum(n9,n3) ),
introduced(definition,[new_symbols(definition,[spl22_96])],[avatar_definition]) ).
fof(f702,plain,
spl22_96,
inference(avatar_split_clause,[],[f98,f699]) ).
fof(f704,definition,
( spl22_97
<=> n0 = sum(n9,n2) ),
introduced(definition,[new_symbols(definition,[spl22_97])],[avatar_definition]) ).
fof(f707,plain,
spl22_97,
inference(avatar_split_clause,[],[f99,f704]) ).
fof(f709,definition,
( spl22_98
<=> n10 = sum(n9,n1) ),
introduced(definition,[new_symbols(definition,[spl22_98])],[avatar_definition]) ).
fof(f712,plain,
spl22_98,
inference(avatar_split_clause,[],[f100,f709]) ).
fof(f714,definition,
( spl22_99
<=> n9 = sum(n9,n0) ),
introduced(definition,[new_symbols(definition,[spl22_99])],[avatar_definition]) ).
fof(f717,plain,
spl22_99,
inference(avatar_split_clause,[],[f101,f714]) ).
fof(f719,definition,
( spl22_100
<=> n7 = sum(n8,n10) ),
introduced(definition,[new_symbols(definition,[spl22_100])],[avatar_definition]) ).
fof(f722,plain,
spl22_100,
inference(avatar_split_clause,[],[f102,f719]) ).
fof(f724,definition,
( spl22_101
<=> n6 = sum(n8,n9) ),
introduced(definition,[new_symbols(definition,[spl22_101])],[avatar_definition]) ).
fof(f727,plain,
spl22_101,
inference(avatar_split_clause,[],[f103,f724]) ).
fof(f729,definition,
( spl22_102
<=> n5 = sum(n8,n8) ),
introduced(definition,[new_symbols(definition,[spl22_102])],[avatar_definition]) ).
fof(f732,plain,
spl22_102,
inference(avatar_split_clause,[],[f104,f729]) ).
fof(f734,definition,
( spl22_103
<=> n4 = sum(n8,n7) ),
introduced(definition,[new_symbols(definition,[spl22_103])],[avatar_definition]) ).
fof(f737,plain,
spl22_103,
inference(avatar_split_clause,[],[f105,f734]) ).
fof(f739,definition,
( spl22_104
<=> n3 = sum(n8,n6) ),
introduced(definition,[new_symbols(definition,[spl22_104])],[avatar_definition]) ).
fof(f742,plain,
spl22_104,
inference(avatar_split_clause,[],[f106,f739]) ).
fof(f744,definition,
( spl22_105
<=> n2 = sum(n8,n5) ),
introduced(definition,[new_symbols(definition,[spl22_105])],[avatar_definition]) ).
fof(f747,plain,
spl22_105,
inference(avatar_split_clause,[],[f107,f744]) ).
fof(f749,definition,
( spl22_106
<=> n1 = sum(n8,n4) ),
introduced(definition,[new_symbols(definition,[spl22_106])],[avatar_definition]) ).
fof(f752,plain,
spl22_106,
inference(avatar_split_clause,[],[f108,f749]) ).
fof(f754,definition,
( spl22_107
<=> n0 = sum(n8,n3) ),
introduced(definition,[new_symbols(definition,[spl22_107])],[avatar_definition]) ).
fof(f757,plain,
spl22_107,
inference(avatar_split_clause,[],[f109,f754]) ).
fof(f759,definition,
( spl22_108
<=> n10 = sum(n8,n2) ),
introduced(definition,[new_symbols(definition,[spl22_108])],[avatar_definition]) ).
fof(f762,plain,
spl22_108,
inference(avatar_split_clause,[],[f110,f759]) ).
fof(f764,definition,
( spl22_109
<=> n9 = sum(n8,n1) ),
introduced(definition,[new_symbols(definition,[spl22_109])],[avatar_definition]) ).
fof(f767,plain,
spl22_109,
inference(avatar_split_clause,[],[f111,f764]) ).
fof(f769,definition,
( spl22_110
<=> n8 = sum(n8,n0) ),
introduced(definition,[new_symbols(definition,[spl22_110])],[avatar_definition]) ).
fof(f772,plain,
spl22_110,
inference(avatar_split_clause,[],[f112,f769]) ).
fof(f774,definition,
( spl22_111
<=> n6 = sum(n7,n10) ),
introduced(definition,[new_symbols(definition,[spl22_111])],[avatar_definition]) ).
fof(f777,plain,
spl22_111,
inference(avatar_split_clause,[],[f113,f774]) ).
fof(f779,definition,
( spl22_112
<=> n5 = sum(n7,n9) ),
introduced(definition,[new_symbols(definition,[spl22_112])],[avatar_definition]) ).
fof(f782,plain,
spl22_112,
inference(avatar_split_clause,[],[f114,f779]) ).
fof(f784,definition,
( spl22_113
<=> n4 = sum(n7,n8) ),
introduced(definition,[new_symbols(definition,[spl22_113])],[avatar_definition]) ).
fof(f787,plain,
spl22_113,
inference(avatar_split_clause,[],[f115,f784]) ).
fof(f789,definition,
( spl22_114
<=> n3 = sum(n7,n7) ),
introduced(definition,[new_symbols(definition,[spl22_114])],[avatar_definition]) ).
fof(f792,plain,
spl22_114,
inference(avatar_split_clause,[],[f116,f789]) ).
fof(f794,definition,
( spl22_115
<=> n2 = sum(n7,n6) ),
introduced(definition,[new_symbols(definition,[spl22_115])],[avatar_definition]) ).
fof(f797,plain,
spl22_115,
inference(avatar_split_clause,[],[f117,f794]) ).
fof(f799,definition,
( spl22_116
<=> n1 = sum(n7,n5) ),
introduced(definition,[new_symbols(definition,[spl22_116])],[avatar_definition]) ).
fof(f802,plain,
spl22_116,
inference(avatar_split_clause,[],[f118,f799]) ).
fof(f804,definition,
( spl22_117
<=> n0 = sum(n7,n4) ),
introduced(definition,[new_symbols(definition,[spl22_117])],[avatar_definition]) ).
fof(f807,plain,
spl22_117,
inference(avatar_split_clause,[],[f119,f804]) ).
fof(f809,definition,
( spl22_118
<=> n10 = sum(n7,n3) ),
introduced(definition,[new_symbols(definition,[spl22_118])],[avatar_definition]) ).
fof(f812,plain,
spl22_118,
inference(avatar_split_clause,[],[f120,f809]) ).
fof(f814,definition,
( spl22_119
<=> n9 = sum(n7,n2) ),
introduced(definition,[new_symbols(definition,[spl22_119])],[avatar_definition]) ).
fof(f817,plain,
spl22_119,
inference(avatar_split_clause,[],[f121,f814]) ).
fof(f819,definition,
( spl22_120
<=> n8 = sum(n7,n1) ),
introduced(definition,[new_symbols(definition,[spl22_120])],[avatar_definition]) ).
fof(f822,plain,
spl22_120,
inference(avatar_split_clause,[],[f122,f819]) ).
fof(f824,definition,
( spl22_121
<=> n7 = sum(n7,n0) ),
introduced(definition,[new_symbols(definition,[spl22_121])],[avatar_definition]) ).
fof(f827,plain,
spl22_121,
inference(avatar_split_clause,[],[f123,f824]) ).
fof(f829,definition,
( spl22_122
<=> n5 = sum(n6,n10) ),
introduced(definition,[new_symbols(definition,[spl22_122])],[avatar_definition]) ).
fof(f832,plain,
spl22_122,
inference(avatar_split_clause,[],[f124,f829]) ).
fof(f834,definition,
( spl22_123
<=> n4 = sum(n6,n9) ),
introduced(definition,[new_symbols(definition,[spl22_123])],[avatar_definition]) ).
fof(f837,plain,
spl22_123,
inference(avatar_split_clause,[],[f125,f834]) ).
fof(f839,definition,
( spl22_124
<=> n3 = sum(n6,n8) ),
introduced(definition,[new_symbols(definition,[spl22_124])],[avatar_definition]) ).
fof(f842,plain,
spl22_124,
inference(avatar_split_clause,[],[f126,f839]) ).
fof(f844,definition,
( spl22_125
<=> n2 = sum(n6,n7) ),
introduced(definition,[new_symbols(definition,[spl22_125])],[avatar_definition]) ).
fof(f847,plain,
spl22_125,
inference(avatar_split_clause,[],[f127,f844]) ).
fof(f849,definition,
( spl22_126
<=> n1 = sum(n6,n6) ),
introduced(definition,[new_symbols(definition,[spl22_126])],[avatar_definition]) ).
fof(f852,plain,
spl22_126,
inference(avatar_split_clause,[],[f128,f849]) ).
fof(f854,definition,
( spl22_127
<=> n0 = sum(n6,n5) ),
introduced(definition,[new_symbols(definition,[spl22_127])],[avatar_definition]) ).
fof(f857,plain,
spl22_127,
inference(avatar_split_clause,[],[f129,f854]) ).
fof(f859,definition,
( spl22_128
<=> n10 = sum(n6,n4) ),
introduced(definition,[new_symbols(definition,[spl22_128])],[avatar_definition]) ).
fof(f862,plain,
spl22_128,
inference(avatar_split_clause,[],[f130,f859]) ).
fof(f864,definition,
( spl22_129
<=> n9 = sum(n6,n3) ),
introduced(definition,[new_symbols(definition,[spl22_129])],[avatar_definition]) ).
fof(f867,plain,
spl22_129,
inference(avatar_split_clause,[],[f131,f864]) ).
fof(f869,definition,
( spl22_130
<=> n8 = sum(n6,n2) ),
introduced(definition,[new_symbols(definition,[spl22_130])],[avatar_definition]) ).
fof(f872,plain,
spl22_130,
inference(avatar_split_clause,[],[f132,f869]) ).
fof(f874,definition,
( spl22_131
<=> n7 = sum(n6,n1) ),
introduced(definition,[new_symbols(definition,[spl22_131])],[avatar_definition]) ).
fof(f877,plain,
spl22_131,
inference(avatar_split_clause,[],[f133,f874]) ).
fof(f879,definition,
( spl22_132
<=> n6 = sum(n6,n0) ),
introduced(definition,[new_symbols(definition,[spl22_132])],[avatar_definition]) ).
fof(f882,plain,
spl22_132,
inference(avatar_split_clause,[],[f134,f879]) ).
fof(f884,definition,
( spl22_133
<=> n4 = sum(n5,n10) ),
introduced(definition,[new_symbols(definition,[spl22_133])],[avatar_definition]) ).
fof(f887,plain,
spl22_133,
inference(avatar_split_clause,[],[f135,f884]) ).
fof(f889,definition,
( spl22_134
<=> n3 = sum(n5,n9) ),
introduced(definition,[new_symbols(definition,[spl22_134])],[avatar_definition]) ).
fof(f892,plain,
spl22_134,
inference(avatar_split_clause,[],[f136,f889]) ).
fof(f894,definition,
( spl22_135
<=> n2 = sum(n5,n8) ),
introduced(definition,[new_symbols(definition,[spl22_135])],[avatar_definition]) ).
fof(f897,plain,
spl22_135,
inference(avatar_split_clause,[],[f137,f894]) ).
fof(f899,definition,
( spl22_136
<=> n1 = sum(n5,n7) ),
introduced(definition,[new_symbols(definition,[spl22_136])],[avatar_definition]) ).
fof(f902,plain,
spl22_136,
inference(avatar_split_clause,[],[f138,f899]) ).
fof(f904,definition,
( spl22_137
<=> n0 = sum(n5,n6) ),
introduced(definition,[new_symbols(definition,[spl22_137])],[avatar_definition]) ).
fof(f907,plain,
spl22_137,
inference(avatar_split_clause,[],[f139,f904]) ).
fof(f909,definition,
( spl22_138
<=> n10 = sum(n5,n5) ),
introduced(definition,[new_symbols(definition,[spl22_138])],[avatar_definition]) ).
fof(f912,plain,
spl22_138,
inference(avatar_split_clause,[],[f140,f909]) ).
fof(f914,definition,
( spl22_139
<=> n9 = sum(n5,n4) ),
introduced(definition,[new_symbols(definition,[spl22_139])],[avatar_definition]) ).
fof(f917,plain,
spl22_139,
inference(avatar_split_clause,[],[f141,f914]) ).
fof(f919,definition,
( spl22_140
<=> n8 = sum(n5,n3) ),
introduced(definition,[new_symbols(definition,[spl22_140])],[avatar_definition]) ).
fof(f922,plain,
spl22_140,
inference(avatar_split_clause,[],[f142,f919]) ).
fof(f924,definition,
( spl22_141
<=> n7 = sum(n5,n2) ),
introduced(definition,[new_symbols(definition,[spl22_141])],[avatar_definition]) ).
fof(f927,plain,
spl22_141,
inference(avatar_split_clause,[],[f143,f924]) ).
fof(f929,definition,
( spl22_142
<=> n6 = sum(n5,n1) ),
introduced(definition,[new_symbols(definition,[spl22_142])],[avatar_definition]) ).
fof(f932,plain,
spl22_142,
inference(avatar_split_clause,[],[f144,f929]) ).
fof(f934,definition,
( spl22_143
<=> n5 = sum(n5,n0) ),
introduced(definition,[new_symbols(definition,[spl22_143])],[avatar_definition]) ).
fof(f937,plain,
spl22_143,
inference(avatar_split_clause,[],[f145,f934]) ).
fof(f939,definition,
( spl22_144
<=> n3 = sum(n4,n10) ),
introduced(definition,[new_symbols(definition,[spl22_144])],[avatar_definition]) ).
fof(f942,plain,
spl22_144,
inference(avatar_split_clause,[],[f146,f939]) ).
fof(f944,definition,
( spl22_145
<=> n2 = sum(n4,n9) ),
introduced(definition,[new_symbols(definition,[spl22_145])],[avatar_definition]) ).
fof(f947,plain,
spl22_145,
inference(avatar_split_clause,[],[f147,f944]) ).
fof(f949,definition,
( spl22_146
<=> n1 = sum(n4,n8) ),
introduced(definition,[new_symbols(definition,[spl22_146])],[avatar_definition]) ).
fof(f952,plain,
spl22_146,
inference(avatar_split_clause,[],[f148,f949]) ).
fof(f954,definition,
( spl22_147
<=> n0 = sum(n4,n7) ),
introduced(definition,[new_symbols(definition,[spl22_147])],[avatar_definition]) ).
fof(f957,plain,
spl22_147,
inference(avatar_split_clause,[],[f149,f954]) ).
fof(f959,definition,
( spl22_148
<=> n10 = sum(n4,n6) ),
introduced(definition,[new_symbols(definition,[spl22_148])],[avatar_definition]) ).
fof(f962,plain,
spl22_148,
inference(avatar_split_clause,[],[f150,f959]) ).
fof(f964,definition,
( spl22_149
<=> n9 = sum(n4,n5) ),
introduced(definition,[new_symbols(definition,[spl22_149])],[avatar_definition]) ).
fof(f967,plain,
spl22_149,
inference(avatar_split_clause,[],[f151,f964]) ).
fof(f969,definition,
( spl22_150
<=> n8 = sum(n4,n4) ),
introduced(definition,[new_symbols(definition,[spl22_150])],[avatar_definition]) ).
fof(f972,plain,
spl22_150,
inference(avatar_split_clause,[],[f152,f969]) ).
fof(f974,definition,
( spl22_151
<=> n7 = sum(n4,n3) ),
introduced(definition,[new_symbols(definition,[spl22_151])],[avatar_definition]) ).
fof(f977,plain,
spl22_151,
inference(avatar_split_clause,[],[f153,f974]) ).
fof(f979,definition,
( spl22_152
<=> n6 = sum(n4,n2) ),
introduced(definition,[new_symbols(definition,[spl22_152])],[avatar_definition]) ).
fof(f982,plain,
spl22_152,
inference(avatar_split_clause,[],[f154,f979]) ).
fof(f984,definition,
( spl22_153
<=> n5 = sum(n4,n1) ),
introduced(definition,[new_symbols(definition,[spl22_153])],[avatar_definition]) ).
fof(f987,plain,
spl22_153,
inference(avatar_split_clause,[],[f155,f984]) ).
fof(f989,definition,
( spl22_154
<=> n4 = sum(n4,n0) ),
introduced(definition,[new_symbols(definition,[spl22_154])],[avatar_definition]) ).
fof(f992,plain,
spl22_154,
inference(avatar_split_clause,[],[f156,f989]) ).
fof(f994,definition,
( spl22_155
<=> n2 = sum(n3,n10) ),
introduced(definition,[new_symbols(definition,[spl22_155])],[avatar_definition]) ).
fof(f997,plain,
spl22_155,
inference(avatar_split_clause,[],[f157,f994]) ).
fof(f999,definition,
( spl22_156
<=> n1 = sum(n3,n9) ),
introduced(definition,[new_symbols(definition,[spl22_156])],[avatar_definition]) ).
fof(f1002,plain,
spl22_156,
inference(avatar_split_clause,[],[f158,f999]) ).
fof(f1004,definition,
( spl22_157
<=> n0 = sum(n3,n8) ),
introduced(definition,[new_symbols(definition,[spl22_157])],[avatar_definition]) ).
fof(f1007,plain,
spl22_157,
inference(avatar_split_clause,[],[f159,f1004]) ).
fof(f1009,definition,
( spl22_158
<=> n10 = sum(n3,n7) ),
introduced(definition,[new_symbols(definition,[spl22_158])],[avatar_definition]) ).
fof(f1012,plain,
spl22_158,
inference(avatar_split_clause,[],[f160,f1009]) ).
fof(f1014,definition,
( spl22_159
<=> n9 = sum(n3,n6) ),
introduced(definition,[new_symbols(definition,[spl22_159])],[avatar_definition]) ).
fof(f1017,plain,
spl22_159,
inference(avatar_split_clause,[],[f161,f1014]) ).
fof(f1019,definition,
( spl22_160
<=> n8 = sum(n3,n5) ),
introduced(definition,[new_symbols(definition,[spl22_160])],[avatar_definition]) ).
fof(f1022,plain,
spl22_160,
inference(avatar_split_clause,[],[f162,f1019]) ).
fof(f1024,definition,
( spl22_161
<=> n7 = sum(n3,n4) ),
introduced(definition,[new_symbols(definition,[spl22_161])],[avatar_definition]) ).
fof(f1027,plain,
spl22_161,
inference(avatar_split_clause,[],[f163,f1024]) ).
fof(f1029,definition,
( spl22_162
<=> n6 = sum(n3,n3) ),
introduced(definition,[new_symbols(definition,[spl22_162])],[avatar_definition]) ).
fof(f1032,plain,
spl22_162,
inference(avatar_split_clause,[],[f164,f1029]) ).
fof(f1034,definition,
( spl22_163
<=> n5 = sum(n3,n2) ),
introduced(definition,[new_symbols(definition,[spl22_163])],[avatar_definition]) ).
fof(f1037,plain,
spl22_163,
inference(avatar_split_clause,[],[f165,f1034]) ).
fof(f1039,definition,
( spl22_164
<=> n4 = sum(n3,n1) ),
introduced(definition,[new_symbols(definition,[spl22_164])],[avatar_definition]) ).
fof(f1042,plain,
spl22_164,
inference(avatar_split_clause,[],[f166,f1039]) ).
fof(f1044,definition,
( spl22_165
<=> n3 = sum(n3,n0) ),
introduced(definition,[new_symbols(definition,[spl22_165])],[avatar_definition]) ).
fof(f1047,plain,
spl22_165,
inference(avatar_split_clause,[],[f167,f1044]) ).
fof(f1049,definition,
( spl22_166
<=> n1 = sum(n2,n10) ),
introduced(definition,[new_symbols(definition,[spl22_166])],[avatar_definition]) ).
fof(f1052,plain,
spl22_166,
inference(avatar_split_clause,[],[f168,f1049]) ).
fof(f1054,definition,
( spl22_167
<=> n0 = sum(n2,n9) ),
introduced(definition,[new_symbols(definition,[spl22_167])],[avatar_definition]) ).
fof(f1057,plain,
spl22_167,
inference(avatar_split_clause,[],[f169,f1054]) ).
fof(f1059,definition,
( spl22_168
<=> n10 = sum(n2,n8) ),
introduced(definition,[new_symbols(definition,[spl22_168])],[avatar_definition]) ).
fof(f1062,plain,
spl22_168,
inference(avatar_split_clause,[],[f170,f1059]) ).
fof(f1064,definition,
( spl22_169
<=> n9 = sum(n2,n7) ),
introduced(definition,[new_symbols(definition,[spl22_169])],[avatar_definition]) ).
fof(f1067,plain,
spl22_169,
inference(avatar_split_clause,[],[f171,f1064]) ).
fof(f1069,definition,
( spl22_170
<=> n8 = sum(n2,n6) ),
introduced(definition,[new_symbols(definition,[spl22_170])],[avatar_definition]) ).
fof(f1072,plain,
spl22_170,
inference(avatar_split_clause,[],[f172,f1069]) ).
fof(f1074,definition,
( spl22_171
<=> n7 = sum(n2,n5) ),
introduced(definition,[new_symbols(definition,[spl22_171])],[avatar_definition]) ).
fof(f1077,plain,
spl22_171,
inference(avatar_split_clause,[],[f173,f1074]) ).
fof(f1079,definition,
( spl22_172
<=> n6 = sum(n2,n4) ),
introduced(definition,[new_symbols(definition,[spl22_172])],[avatar_definition]) ).
fof(f1082,plain,
spl22_172,
inference(avatar_split_clause,[],[f174,f1079]) ).
fof(f1084,definition,
( spl22_173
<=> n5 = sum(n2,n3) ),
introduced(definition,[new_symbols(definition,[spl22_173])],[avatar_definition]) ).
fof(f1087,plain,
spl22_173,
inference(avatar_split_clause,[],[f175,f1084]) ).
fof(f1089,definition,
( spl22_174
<=> n4 = sum(n2,n2) ),
introduced(definition,[new_symbols(definition,[spl22_174])],[avatar_definition]) ).
fof(f1092,plain,
spl22_174,
inference(avatar_split_clause,[],[f176,f1089]) ).
fof(f1094,definition,
( spl22_175
<=> n3 = sum(n2,n1) ),
introduced(definition,[new_symbols(definition,[spl22_175])],[avatar_definition]) ).
fof(f1097,plain,
spl22_175,
inference(avatar_split_clause,[],[f177,f1094]) ).
fof(f1099,definition,
( spl22_176
<=> n2 = sum(n2,n0) ),
introduced(definition,[new_symbols(definition,[spl22_176])],[avatar_definition]) ).
fof(f1102,plain,
spl22_176,
inference(avatar_split_clause,[],[f178,f1099]) ).
fof(f1104,definition,
( spl22_177
<=> n0 = sum(n1,n10) ),
introduced(definition,[new_symbols(definition,[spl22_177])],[avatar_definition]) ).
fof(f1107,plain,
spl22_177,
inference(avatar_split_clause,[],[f179,f1104]) ).
fof(f1109,definition,
( spl22_178
<=> n10 = sum(n1,n9) ),
introduced(definition,[new_symbols(definition,[spl22_178])],[avatar_definition]) ).
fof(f1112,plain,
spl22_178,
inference(avatar_split_clause,[],[f180,f1109]) ).
fof(f1114,definition,
( spl22_179
<=> n9 = sum(n1,n8) ),
introduced(definition,[new_symbols(definition,[spl22_179])],[avatar_definition]) ).
fof(f1117,plain,
spl22_179,
inference(avatar_split_clause,[],[f181,f1114]) ).
fof(f1119,definition,
( spl22_180
<=> n8 = sum(n1,n7) ),
introduced(definition,[new_symbols(definition,[spl22_180])],[avatar_definition]) ).
fof(f1122,plain,
spl22_180,
inference(avatar_split_clause,[],[f182,f1119]) ).
fof(f1124,definition,
( spl22_181
<=> n7 = sum(n1,n6) ),
introduced(definition,[new_symbols(definition,[spl22_181])],[avatar_definition]) ).
fof(f1127,plain,
spl22_181,
inference(avatar_split_clause,[],[f183,f1124]) ).
fof(f1129,definition,
( spl22_182
<=> n6 = sum(n1,n5) ),
introduced(definition,[new_symbols(definition,[spl22_182])],[avatar_definition]) ).
fof(f1132,plain,
spl22_182,
inference(avatar_split_clause,[],[f184,f1129]) ).
fof(f1134,definition,
( spl22_183
<=> n5 = sum(n1,n4) ),
introduced(definition,[new_symbols(definition,[spl22_183])],[avatar_definition]) ).
fof(f1137,plain,
spl22_183,
inference(avatar_split_clause,[],[f185,f1134]) ).
fof(f1139,definition,
( spl22_184
<=> n4 = sum(n1,n3) ),
introduced(definition,[new_symbols(definition,[spl22_184])],[avatar_definition]) ).
fof(f1142,plain,
spl22_184,
inference(avatar_split_clause,[],[f186,f1139]) ).
fof(f1144,definition,
( spl22_185
<=> n3 = sum(n1,n2) ),
introduced(definition,[new_symbols(definition,[spl22_185])],[avatar_definition]) ).
fof(f1147,plain,
spl22_185,
inference(avatar_split_clause,[],[f187,f1144]) ).
fof(f1149,definition,
( spl22_186
<=> n2 = sum(n1,n1) ),
introduced(definition,[new_symbols(definition,[spl22_186])],[avatar_definition]) ).
fof(f1152,plain,
spl22_186,
inference(avatar_split_clause,[],[f188,f1149]) ).
fof(f1154,definition,
( spl22_187
<=> n1 = sum(n1,n0) ),
introduced(definition,[new_symbols(definition,[spl22_187])],[avatar_definition]) ).
fof(f1157,plain,
spl22_187,
inference(avatar_split_clause,[],[f189,f1154]) ).
fof(f1159,definition,
( spl22_188
<=> n10 = sum(n0,n10) ),
introduced(definition,[new_symbols(definition,[spl22_188])],[avatar_definition]) ).
fof(f1162,plain,
spl22_188,
inference(avatar_split_clause,[],[f190,f1159]) ).
fof(f1164,definition,
( spl22_189
<=> n9 = sum(n0,n9) ),
introduced(definition,[new_symbols(definition,[spl22_189])],[avatar_definition]) ).
fof(f1167,plain,
spl22_189,
inference(avatar_split_clause,[],[f191,f1164]) ).
fof(f1169,definition,
( spl22_190
<=> n8 = sum(n0,n8) ),
introduced(definition,[new_symbols(definition,[spl22_190])],[avatar_definition]) ).
fof(f1172,plain,
spl22_190,
inference(avatar_split_clause,[],[f192,f1169]) ).
fof(f1174,definition,
( spl22_191
<=> n7 = sum(n0,n7) ),
introduced(definition,[new_symbols(definition,[spl22_191])],[avatar_definition]) ).
fof(f1177,plain,
spl22_191,
inference(avatar_split_clause,[],[f193,f1174]) ).
fof(f1179,definition,
( spl22_192
<=> n6 = sum(n0,n6) ),
introduced(definition,[new_symbols(definition,[spl22_192])],[avatar_definition]) ).
fof(f1182,plain,
spl22_192,
inference(avatar_split_clause,[],[f194,f1179]) ).
fof(f1184,definition,
( spl22_193
<=> n5 = sum(n0,n5) ),
introduced(definition,[new_symbols(definition,[spl22_193])],[avatar_definition]) ).
fof(f1187,plain,
spl22_193,
inference(avatar_split_clause,[],[f195,f1184]) ).
fof(f1189,definition,
( spl22_194
<=> n4 = sum(n0,n4) ),
introduced(definition,[new_symbols(definition,[spl22_194])],[avatar_definition]) ).
fof(f1192,plain,
spl22_194,
inference(avatar_split_clause,[],[f196,f1189]) ).
fof(f1194,definition,
( spl22_195
<=> n3 = sum(n0,n3) ),
introduced(definition,[new_symbols(definition,[spl22_195])],[avatar_definition]) ).
fof(f1197,plain,
spl22_195,
inference(avatar_split_clause,[],[f197,f1194]) ).
fof(f1199,definition,
( spl22_196
<=> n2 = sum(n0,n2) ),
introduced(definition,[new_symbols(definition,[spl22_196])],[avatar_definition]) ).
fof(f1202,plain,
spl22_196,
inference(avatar_split_clause,[],[f198,f1199]) ).
fof(f1204,definition,
( spl22_197
<=> n1 = sum(n0,n1) ),
introduced(definition,[new_symbols(definition,[spl22_197])],[avatar_definition]) ).
fof(f1207,plain,
spl22_197,
inference(avatar_split_clause,[],[f199,f1204]) ).
fof(f1209,definition,
( spl22_198
<=> n0 = sum(n0,n0) ),
introduced(definition,[new_symbols(definition,[spl22_198])],[avatar_definition]) ).
fof(f1212,plain,
spl22_198,
inference(avatar_split_clause,[],[f200,f1209]) ).
fof(f1214,definition,
( spl22_199
<=> sK21 = sum(sum(pred(sK18),succ(sK18)),sum(pred(sK19),succ(sK19))) ),
introduced(definition,[new_symbols(definition,[spl22_199])],[avatar_definition]) ).
fof(f1217,plain,
spl22_199,
inference(avatar_split_clause,[],[f60,f1214]) ).
fof(f1219,definition,
( spl22_200
<=> sK20 = sum(sum(pred(sK18),succ(sK19)),sum(pred(sK19),succ(sK18))) ),
introduced(definition,[new_symbols(definition,[spl22_200])],[avatar_definition]) ).
fof(f1222,plain,
spl22_200,
inference(avatar_split_clause,[],[f61,f1219]) ).
fof(f1224,definition,
( spl22_201
<=> sK19 = sum(sum(pred(sK16),succ(sK16)),sum(pred(sK17),succ(sK17))) ),
introduced(definition,[new_symbols(definition,[spl22_201])],[avatar_definition]) ).
fof(f1227,plain,
spl22_201,
inference(avatar_split_clause,[],[f62,f1224]) ).
fof(f1229,definition,
( spl22_202
<=> sK18 = sum(sum(pred(sK16),succ(sK17)),sum(pred(sK17),succ(sK16))) ),
introduced(definition,[new_symbols(definition,[spl22_202])],[avatar_definition]) ).
fof(f1232,plain,
spl22_202,
inference(avatar_split_clause,[],[f63,f1229]) ).
fof(f1234,definition,
( spl22_203
<=> sK17 = sum(sum(pred(sK14),succ(sK14)),sum(pred(sK15),succ(sK15))) ),
introduced(definition,[new_symbols(definition,[spl22_203])],[avatar_definition]) ).
fof(f1237,plain,
spl22_203,
inference(avatar_split_clause,[],[f64,f1234]) ).
fof(f1239,definition,
( spl22_204
<=> sK16 = sum(sum(pred(sK14),succ(sK15)),sum(pred(sK15),succ(sK14))) ),
introduced(definition,[new_symbols(definition,[spl22_204])],[avatar_definition]) ).
fof(f1242,plain,
spl22_204,
inference(avatar_split_clause,[],[f65,f1239]) ).
fof(f1244,definition,
( spl22_205
<=> sK15 = sum(sum(pred(sK12),succ(sK12)),sum(pred(sK13),succ(sK13))) ),
introduced(definition,[new_symbols(definition,[spl22_205])],[avatar_definition]) ).
fof(f1247,plain,
spl22_205,
inference(avatar_split_clause,[],[f66,f1244]) ).
fof(f1249,definition,
( spl22_206
<=> sK14 = sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12))) ),
introduced(definition,[new_symbols(definition,[spl22_206])],[avatar_definition]) ).
fof(f1252,plain,
spl22_206,
inference(avatar_split_clause,[],[f67,f1249]) ).
fof(f1254,definition,
( spl22_207
<=> sK13 = sum(sum(pred(sK10),succ(sK10)),sum(pred(sK11),succ(sK11))) ),
introduced(definition,[new_symbols(definition,[spl22_207])],[avatar_definition]) ).
fof(f1257,plain,
spl22_207,
inference(avatar_split_clause,[],[f68,f1254]) ).
fof(f1259,definition,
( spl22_208
<=> sK12 = sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10))) ),
introduced(definition,[new_symbols(definition,[spl22_208])],[avatar_definition]) ).
fof(f1262,plain,
spl22_208,
inference(avatar_split_clause,[],[f69,f1259]) ).
fof(f1264,definition,
( spl22_209
<=> sK11 = sum(sum(pred(sK8),succ(sK8)),sum(pred(sK9),succ(sK9))) ),
introduced(definition,[new_symbols(definition,[spl22_209])],[avatar_definition]) ).
fof(f1267,plain,
spl22_209,
inference(avatar_split_clause,[],[f70,f1264]) ).
fof(f1269,definition,
( spl22_210
<=> sK10 = sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8))) ),
introduced(definition,[new_symbols(definition,[spl22_210])],[avatar_definition]) ).
fof(f1272,plain,
spl22_210,
inference(avatar_split_clause,[],[f71,f1269]) ).
fof(f1274,definition,
( spl22_211
<=> sK9 = sum(sum(pred(sK6),succ(sK6)),sum(pred(sK7),succ(sK7))) ),
introduced(definition,[new_symbols(definition,[spl22_211])],[avatar_definition]) ).
fof(f1277,plain,
spl22_211,
inference(avatar_split_clause,[],[f72,f1274]) ).
fof(f1279,definition,
( spl22_212
<=> sK8 = sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6))) ),
introduced(definition,[new_symbols(definition,[spl22_212])],[avatar_definition]) ).
fof(f1282,plain,
spl22_212,
inference(avatar_split_clause,[],[f73,f1279]) ).
fof(f1284,definition,
( spl22_213
<=> sK7 = sum(sum(pred(sK4),succ(sK4)),sum(pred(sK5),succ(sK5))) ),
introduced(definition,[new_symbols(definition,[spl22_213])],[avatar_definition]) ).
fof(f1287,plain,
spl22_213,
inference(avatar_split_clause,[],[f74,f1284]) ).
fof(f1289,definition,
( spl22_214
<=> sK6 = sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4))) ),
introduced(definition,[new_symbols(definition,[spl22_214])],[avatar_definition]) ).
fof(f1292,plain,
spl22_214,
inference(avatar_split_clause,[],[f75,f1289]) ).
fof(f1294,definition,
( spl22_215
<=> sK5 = sum(sum(pred(sK2),succ(sK2)),sum(pred(sK3),succ(sK3))) ),
introduced(definition,[new_symbols(definition,[spl22_215])],[avatar_definition]) ).
fof(f1297,plain,
spl22_215,
inference(avatar_split_clause,[],[f76,f1294]) ).
fof(f1299,definition,
( spl22_216
<=> sK4 = sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2))) ),
introduced(definition,[new_symbols(definition,[spl22_216])],[avatar_definition]) ).
fof(f1302,plain,
spl22_216,
inference(avatar_split_clause,[],[f77,f1299]) ).
fof(f1304,definition,
( spl22_217
<=> sK3 = sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1))) ),
introduced(definition,[new_symbols(definition,[spl22_217])],[avatar_definition]) ).
fof(f1307,plain,
spl22_217,
inference(avatar_split_clause,[],[f78,f1304]) ).
fof(f1309,definition,
( spl22_218
<=> sK2 = sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0))) ),
introduced(definition,[new_symbols(definition,[spl22_218])],[avatar_definition]) ).
fof(f1312,plain,
spl22_218,
inference(avatar_split_clause,[],[f79,f1309]) ).
fof(f1314,definition,
( spl22_219
<=> sK2 = sK3 ),
introduced(definition,[new_symbols(definition,[spl22_219])],[avatar_definition]) ).
fof(f1318,definition,
( spl22_220
<=> sK4 = sK5 ),
introduced(definition,[new_symbols(definition,[spl22_220])],[avatar_definition]) ).
fof(f1322,definition,
( spl22_221
<=> sK6 = sK7 ),
introduced(definition,[new_symbols(definition,[spl22_221])],[avatar_definition]) ).
fof(f1326,definition,
( spl22_222
<=> sK8 = sK9 ),
introduced(definition,[new_symbols(definition,[spl22_222])],[avatar_definition]) ).
fof(f1330,definition,
( spl22_223
<=> sK10 = sK11 ),
introduced(definition,[new_symbols(definition,[spl22_223])],[avatar_definition]) ).
fof(f1334,definition,
( spl22_224
<=> sK12 = sK13 ),
introduced(definition,[new_symbols(definition,[spl22_224])],[avatar_definition]) ).
fof(f1338,definition,
( spl22_225
<=> sK14 = sK15 ),
introduced(definition,[new_symbols(definition,[spl22_225])],[avatar_definition]) ).
fof(f1342,definition,
( spl22_226
<=> sK16 = sK17 ),
introduced(definition,[new_symbols(definition,[spl22_226])],[avatar_definition]) ).
fof(f1346,definition,
( spl22_227
<=> sK18 = sK19 ),
introduced(definition,[new_symbols(definition,[spl22_227])],[avatar_definition]) ).
fof(f1350,definition,
( spl22_228
<=> sK20 = sK21 ),
introduced(definition,[new_symbols(definition,[spl22_228])],[avatar_definition]) ).
fof(f1353,plain,
( ~ spl22_219
| ~ spl22_220
| ~ spl22_221
| ~ spl22_222
| ~ spl22_223
| ~ spl22_224
| ~ spl22_225
| ~ spl22_226
| ~ spl22_227
| ~ spl22_228 ),
inference(avatar_split_clause,[],[f4,f1350,f1346,f1342,f1338,f1334,f1330,f1326,f1322,f1318,f1314]) ).
fof(f1355,definition,
( spl22_229
<=> n0 = sK0 ),
introduced(definition,[new_symbols(definition,[spl22_229])],[avatar_definition]) ).
fof(f1359,definition,
( spl22_230
<=> n1 = sK0 ),
introduced(definition,[new_symbols(definition,[spl22_230])],[avatar_definition]) ).
fof(f1363,definition,
( spl22_231
<=> n2 = sK0 ),
introduced(definition,[new_symbols(definition,[spl22_231])],[avatar_definition]) ).
fof(f1367,definition,
( spl22_232
<=> n3 = sK0 ),
introduced(definition,[new_symbols(definition,[spl22_232])],[avatar_definition]) ).
fof(f1371,definition,
( spl22_233
<=> n4 = sK0 ),
introduced(definition,[new_symbols(definition,[spl22_233])],[avatar_definition]) ).
fof(f1375,definition,
( spl22_234
<=> n5 = sK0 ),
introduced(definition,[new_symbols(definition,[spl22_234])],[avatar_definition]) ).
fof(f1379,definition,
( spl22_235
<=> n6 = sK0 ),
introduced(definition,[new_symbols(definition,[spl22_235])],[avatar_definition]) ).
fof(f1383,definition,
( spl22_236
<=> n7 = sK0 ),
introduced(definition,[new_symbols(definition,[spl22_236])],[avatar_definition]) ).
fof(f1387,definition,
( spl22_237
<=> n8 = sK0 ),
introduced(definition,[new_symbols(definition,[spl22_237])],[avatar_definition]) ).
fof(f1391,definition,
( spl22_238
<=> n9 = sK0 ),
introduced(definition,[new_symbols(definition,[spl22_238])],[avatar_definition]) ).
fof(f1395,definition,
( spl22_239
<=> n10 = sK0 ),
introduced(definition,[new_symbols(definition,[spl22_239])],[avatar_definition]) ).
fof(f1398,plain,
( spl22_229
| spl22_230
| spl22_231
| spl22_232
| spl22_233
| spl22_234
| spl22_235
| spl22_236
| spl22_237
| spl22_238
| spl22_239 ),
inference(avatar_split_clause,[],[f2,f1395,f1391,f1387,f1383,f1379,f1375,f1371,f1367,f1363,f1359,f1355]) ).
fof(f1400,definition,
( spl22_240
<=> n0 = sK1 ),
introduced(definition,[new_symbols(definition,[spl22_240])],[avatar_definition]) ).
fof(f1404,definition,
( spl22_241
<=> n1 = sK1 ),
introduced(definition,[new_symbols(definition,[spl22_241])],[avatar_definition]) ).
fof(f1408,definition,
( spl22_242
<=> n2 = sK1 ),
introduced(definition,[new_symbols(definition,[spl22_242])],[avatar_definition]) ).
fof(f1412,definition,
( spl22_243
<=> n3 = sK1 ),
introduced(definition,[new_symbols(definition,[spl22_243])],[avatar_definition]) ).
fof(f1416,definition,
( spl22_244
<=> n4 = sK1 ),
introduced(definition,[new_symbols(definition,[spl22_244])],[avatar_definition]) ).
fof(f1420,definition,
( spl22_245
<=> n5 = sK1 ),
introduced(definition,[new_symbols(definition,[spl22_245])],[avatar_definition]) ).
fof(f1424,definition,
( spl22_246
<=> n6 = sK1 ),
introduced(definition,[new_symbols(definition,[spl22_246])],[avatar_definition]) ).
fof(f1428,definition,
( spl22_247
<=> n7 = sK1 ),
introduced(definition,[new_symbols(definition,[spl22_247])],[avatar_definition]) ).
fof(f1432,definition,
( spl22_248
<=> n8 = sK1 ),
introduced(definition,[new_symbols(definition,[spl22_248])],[avatar_definition]) ).
fof(f1436,definition,
( spl22_249
<=> n9 = sK1 ),
introduced(definition,[new_symbols(definition,[spl22_249])],[avatar_definition]) ).
fof(f1440,definition,
( spl22_250
<=> n10 = sK1 ),
introduced(definition,[new_symbols(definition,[spl22_250])],[avatar_definition]) ).
fof(f1443,plain,
( spl22_240
| spl22_241
| spl22_242
| spl22_243
| spl22_244
| spl22_245
| spl22_246
| spl22_247
| spl22_248
| spl22_249
| spl22_250 ),
inference(avatar_split_clause,[],[f3,f1440,f1436,f1432,f1428,f1424,f1420,f1416,f1412,f1408,f1404,f1400]) ).
fof(f1444,plain,
( n0 != sK1
| n10 != pred(n0)
| n0 != sK0
| succ(n0) != n1
| n0 != sum(n10,n1)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1445,plain,
( sK2 != sK3
| sK5 != sum(sum(pred(sK2),succ(sK2)),sum(pred(sK3),succ(sK3)))
| sK4 != sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2)))
| sK7 != sum(sum(pred(sK4),succ(sK4)),sum(pred(sK5),succ(sK5)))
| sK6 != sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4)))
| sK8 != sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6)))
| sK9 != sum(sum(pred(sK6),succ(sK6)),sum(pred(sK7),succ(sK7)))
| sK11 != sum(sum(pred(sK8),succ(sK8)),sum(pred(sK9),succ(sK9)))
| sK10 != sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8)))
| sK12 != sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10)))
| sK13 != sum(sum(pred(sK10),succ(sK10)),sum(pred(sK11),succ(sK11)))
| sK15 != sum(sum(pred(sK12),succ(sK12)),sum(pred(sK13),succ(sK13)))
| sK14 != sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12)))
| sK16 != sum(sum(pred(sK14),succ(sK15)),sum(pred(sK15),succ(sK14)))
| sK17 != sum(sum(pred(sK14),succ(sK14)),sum(pred(sK15),succ(sK15)))
| sK19 != sum(sum(pred(sK16),succ(sK16)),sum(pred(sK17),succ(sK17)))
| sK18 != sum(sum(pred(sK16),succ(sK17)),sum(pred(sK17),succ(sK16)))
| sK20 != sum(sum(pred(sK18),succ(sK19)),sum(pred(sK19),succ(sK18)))
| sK21 != sum(sum(pred(sK18),succ(sK18)),sum(pred(sK19),succ(sK19)))
| sK20 = sK21 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1446,plain,
( sK2 != sK3
| sK5 != sum(sum(pred(sK2),succ(sK2)),sum(pred(sK3),succ(sK3)))
| sK4 != sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2)))
| sK4 = sK5 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1447,plain,
( n2 != sum(n0,n2)
| n0 != sum(n10,n1)
| n0 != pred(n1)
| succ(n0) != n1
| n1 != sum(n0,n1)
| n0 != sK1
| n10 != pred(n0)
| n1 != sK0
| succ(n1) != n2
| n1 != sum(n10,n2)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n2 != sum(n1,n1)
| n2 != sum(n2,n0)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1449,plain,
( n4 != sum(n1,n3)
| n0 != sum(n10,n1)
| n1 != pred(n2)
| succ(n0) != n1
| n2 != sum(n1,n1)
| n0 != sK1
| n10 != pred(n0)
| n2 != sK0
| succ(n2) != n3
| n2 != sum(n10,n3)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n4 != sum(n2,n2)
| n4 != sum(n4,n0)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1451,plain,
( n6 != sum(n2,n4)
| n0 != sum(n10,n1)
| n2 != pred(n3)
| succ(n0) != n1
| n3 != sum(n2,n1)
| n0 != sK1
| n10 != pred(n0)
| n3 != sK0
| succ(n3) != n4
| n3 != sum(n10,n4)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n6 != sum(n3,n3)
| n6 != sum(n6,n0)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1453,plain,
( n8 != sum(n3,n5)
| n0 != sum(n10,n1)
| n3 != pred(n4)
| succ(n0) != n1
| n4 != sum(n3,n1)
| n0 != sK1
| n10 != pred(n0)
| n4 != sK0
| succ(n4) != n5
| n4 != sum(n10,n5)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n8 != sum(n4,n4)
| n8 != sum(n8,n0)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1455,plain,
( n10 != sum(n4,n6)
| n0 != sum(n10,n1)
| n4 != pred(n5)
| succ(n0) != n1
| n5 != sum(n4,n1)
| n0 != sK1
| n10 != pred(n0)
| n5 != sK0
| succ(n5) != n6
| n5 != sum(n10,n6)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n10 != sum(n5,n5)
| n10 != sum(n10,n0)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1457,plain,
( sK2 != sK3
| sK4 != sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2)))
| sK5 != sum(sum(pred(sK2),succ(sK2)),sum(pred(sK3),succ(sK3)))
| sK7 != sum(sum(pred(sK4),succ(sK4)),sum(pred(sK5),succ(sK5)))
| sK6 != sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4)))
| sK9 != sum(sum(pred(sK6),succ(sK6)),sum(pred(sK7),succ(sK7)))
| sK8 != sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6)))
| sK11 != sum(sum(pred(sK8),succ(sK8)),sum(pred(sK9),succ(sK9)))
| sK10 != sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8)))
| sK12 != sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10)))
| sK13 != sum(sum(pred(sK10),succ(sK10)),sum(pred(sK11),succ(sK11)))
| sK15 != sum(sum(pred(sK12),succ(sK12)),sum(pred(sK13),succ(sK13)))
| sK14 != sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12)))
| sK16 != sum(sum(pred(sK14),succ(sK15)),sum(pred(sK15),succ(sK14)))
| sK17 != sum(sum(pred(sK14),succ(sK14)),sum(pred(sK15),succ(sK15)))
| sK19 != sum(sum(pred(sK16),succ(sK16)),sum(pred(sK17),succ(sK17)))
| sK18 != sum(sum(pred(sK16),succ(sK17)),sum(pred(sK17),succ(sK16)))
| sK18 = sK19 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1458,plain,
( n10 != sum(n4,n6)
| n2 != sum(n0,n2)
| n4 != pred(n5)
| succ(n1) != n2
| n6 != sum(n4,n2)
| n1 != sK1
| n0 != pred(n1)
| n5 != sK0
| succ(n5) != n6
| n6 != sum(n0,n6)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n1 != sum(n6,n6)
| n1 != sum(n10,n2)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1460,plain,
( n10 != sum(n4,n6)
| n4 != sum(n1,n3)
| n4 != pred(n5)
| succ(n2) != n3
| n7 != sum(n4,n3)
| n2 != sK1
| n1 != pred(n2)
| n5 != sK0
| succ(n5) != n6
| n7 != sum(n1,n6)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n3 != sum(n7,n7)
| n3 != sum(n10,n4)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1463,plain,
( n10 != sum(n4,n6)
| n6 != sum(n2,n4)
| n4 != pred(n5)
| succ(n3) != n4
| n8 != sum(n4,n4)
| n3 != sK1
| n2 != pred(n3)
| n5 != sK0
| succ(n5) != n6
| n8 != sum(n2,n6)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n5 != sum(n8,n8)
| n5 != sum(n10,n6)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1466,plain,
( n10 != sum(n4,n6)
| n8 != sum(n3,n5)
| n4 != pred(n5)
| succ(n4) != n5
| n9 != sum(n4,n5)
| n4 != sK1
| n3 != pred(n4)
| n5 != sK0
| succ(n5) != n6
| n9 != sum(n3,n6)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n7 != sum(n9,n9)
| n7 != sum(n10,n8)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1469,plain,
( n5 != sK1
| n4 != pred(n5)
| n5 != sK0
| succ(n5) != n6
| n10 != sum(n4,n6)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1472,plain,
( n10 != sum(n4,n6)
| n1 != sum(n5,n7)
| n4 != pred(n5)
| succ(n6) != n7
| n0 != sum(n4,n7)
| n6 != sK1
| n5 != pred(n6)
| n5 != sK0
| succ(n5) != n6
| n0 != sum(n5,n6)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n0 != sum(n0,n0)
| n0 != sum(n10,n1)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1475,plain,
( n10 != sum(n4,n6)
| n3 != sum(n6,n8)
| n4 != pred(n5)
| succ(n7) != n8
| n1 != sum(n4,n8)
| n7 != sK1
| n6 != pred(n7)
| n5 != sK0
| succ(n5) != n6
| n1 != sum(n6,n6)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n2 != sum(n1,n1)
| n2 != sum(n10,n3)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1478,plain,
( n10 != sum(n4,n6)
| n5 != sum(n7,n9)
| n4 != pred(n5)
| succ(n8) != n9
| n2 != sum(n4,n9)
| n8 != sK1
| n7 != pred(n8)
| n5 != sK0
| succ(n5) != n6
| n2 != sum(n7,n6)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n4 != sum(n2,n2)
| n4 != sum(n10,n5)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1481,plain,
( n10 != sum(n4,n6)
| n7 != sum(n8,n10)
| n4 != pred(n5)
| succ(n9) != n10
| n3 != sum(n4,n10)
| n9 != sK1
| n8 != pred(n9)
| n5 != sK0
| succ(n5) != n6
| n3 != sum(n8,n6)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n6 != sum(n3,n3)
| n6 != sum(n10,n7)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1484,plain,
( n10 != sum(n4,n6)
| n9 != sum(n9,n0)
| n4 != pred(n5)
| n0 != succ(n10)
| n4 != sum(n4,n0)
| n10 != sK1
| n9 != pred(n10)
| n5 != sK0
| succ(n5) != n6
| n4 != sum(n9,n6)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n8 != sum(n4,n4)
| n8 != sum(n10,n9)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1487,plain,
( sK2 != sK3
| sK5 != sum(sum(pred(sK2),succ(sK2)),sum(pred(sK3),succ(sK3)))
| sK4 != sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2)))
| sK7 != sum(sum(pred(sK4),succ(sK4)),sum(pred(sK5),succ(sK5)))
| sK6 != sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4)))
| sK9 != sum(sum(pred(sK6),succ(sK6)),sum(pred(sK7),succ(sK7)))
| sK8 != sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6)))
| sK8 = sK9 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1488,plain,
( sK2 != sK3
| sK5 != sum(sum(pred(sK2),succ(sK2)),sum(pred(sK3),succ(sK3)))
| sK4 != sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2)))
| sK7 != sum(sum(pred(sK4),succ(sK4)),sum(pred(sK5),succ(sK5)))
| sK6 != sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4)))
| sK6 = sK7 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1489,plain,
( sK2 != sK3
| sK5 != sum(sum(pred(sK2),succ(sK2)),sum(pred(sK3),succ(sK3)))
| sK4 != sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2)))
| sK7 != sum(sum(pred(sK4),succ(sK4)),sum(pred(sK5),succ(sK5)))
| sK6 != sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4)))
| sK9 != sum(sum(pred(sK6),succ(sK6)),sum(pred(sK7),succ(sK7)))
| sK8 != sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6)))
| sK11 != sum(sum(pred(sK8),succ(sK8)),sum(pred(sK9),succ(sK9)))
| sK10 != sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8)))
| sK12 != sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10)))
| sK13 != sum(sum(pred(sK10),succ(sK10)),sum(pred(sK11),succ(sK11)))
| sK15 != sum(sum(pred(sK12),succ(sK12)),sum(pred(sK13),succ(sK13)))
| sK14 != sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12)))
| sK16 != sum(sum(pred(sK14),succ(sK15)),sum(pred(sK15),succ(sK14)))
| sK17 != sum(sum(pred(sK14),succ(sK14)),sum(pred(sK15),succ(sK15)))
| sK16 = sK17 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1490,plain,
( sK2 != sK3
| sK5 != sum(sum(pred(sK2),succ(sK2)),sum(pred(sK3),succ(sK3)))
| sK4 != sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2)))
| sK7 != sum(sum(pred(sK4),succ(sK4)),sum(pred(sK5),succ(sK5)))
| sK6 != sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4)))
| sK9 != sum(sum(pred(sK6),succ(sK6)),sum(pred(sK7),succ(sK7)))
| sK8 != sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6)))
| sK11 != sum(sum(pred(sK8),succ(sK8)),sum(pred(sK9),succ(sK9)))
| sK10 != sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8)))
| sK10 = sK11 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1491,plain,
( sK2 != sK3
| sK5 != sum(sum(pred(sK2),succ(sK2)),sum(pred(sK3),succ(sK3)))
| sK4 != sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2)))
| sK7 != sum(sum(pred(sK4),succ(sK4)),sum(pred(sK5),succ(sK5)))
| sK6 != sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4)))
| sK9 != sum(sum(pred(sK6),succ(sK6)),sum(pred(sK7),succ(sK7)))
| sK8 != sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6)))
| sK11 != sum(sum(pred(sK8),succ(sK8)),sum(pred(sK9),succ(sK9)))
| sK10 != sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8)))
| sK12 != sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10)))
| sK13 != sum(sum(pred(sK10),succ(sK10)),sum(pred(sK11),succ(sK11)))
| sK15 != sum(sum(pred(sK12),succ(sK12)),sum(pred(sK13),succ(sK13)))
| sK14 != sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12)))
| sK14 = sK15 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1492,plain,
( sK2 != sK3
| sK5 != sum(sum(pred(sK2),succ(sK2)),sum(pred(sK3),succ(sK3)))
| sK4 != sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2)))
| sK7 != sum(sum(pred(sK4),succ(sK4)),sum(pred(sK5),succ(sK5)))
| sK6 != sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4)))
| sK9 != sum(sum(pred(sK6),succ(sK6)),sum(pred(sK7),succ(sK7)))
| sK8 != sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6)))
| sK11 != sum(sum(pred(sK8),succ(sK8)),sum(pred(sK9),succ(sK9)))
| sK10 != sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8)))
| sK12 != sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10)))
| sK13 != sum(sum(pred(sK10),succ(sK10)),sum(pred(sK11),succ(sK11)))
| sK12 = sK13 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1493,plain,
( n2 != sum(n0,n2)
| n5 != sum(n7,n9)
| n0 != pred(n1)
| succ(n8) != n9
| n9 != sum(n0,n9)
| n8 != sK1
| n7 != pred(n8)
| n1 != sK0
| succ(n1) != n2
| n9 != sum(n7,n2)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n7 != sum(n9,n9)
| n7 != sum(n2,n5)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1494,plain,
( n0 != sum(n10,n1)
| n5 != sum(n7,n9)
| n10 != pred(n0)
| succ(n8) != n9
| n8 != sum(n10,n9)
| n8 != sK1
| n7 != pred(n8)
| n0 != sK0
| succ(n0) != n1
| n8 != sum(n7,n1)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n5 != sum(n8,n8)
| n5 != sum(n0,n5)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1495,plain,
( n3 != sum(n6,n8)
| n5 != sum(n7,n9)
| n6 != pred(n7)
| succ(n8) != n9
| n4 != sum(n6,n9)
| n8 != sK1
| n7 != pred(n8)
| n7 != sK0
| succ(n7) != n8
| n4 != sum(n7,n8)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n8 != sum(n4,n4)
| n8 != sum(n3,n5)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1496,plain,
( n1 != sum(n5,n7)
| n5 != sum(n7,n9)
| n5 != pred(n6)
| succ(n8) != n9
| n3 != sum(n5,n9)
| n8 != sK1
| n7 != pred(n8)
| n6 != sK0
| succ(n6) != n7
| n3 != sum(n7,n7)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n6 != sum(n3,n3)
| n6 != sum(n1,n5)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1497,plain,
( n6 != sum(n2,n4)
| n5 != sum(n7,n9)
| n2 != pred(n3)
| succ(n8) != n9
| n0 != sum(n2,n9)
| n8 != sK1
| n7 != pred(n8)
| n3 != sK0
| succ(n3) != n4
| n0 != sum(n7,n4)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n0 != sum(n0,n0)
| n0 != sum(n6,n5)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1498,plain,
( n9 != sum(n9,n0)
| n5 != sum(n7,n9)
| n9 != pred(n10)
| succ(n8) != n9
| n7 != sum(n9,n9)
| n8 != sK1
| n7 != pred(n8)
| n10 != sK0
| n0 != succ(n10)
| n7 != sum(n7,n0)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n3 != sum(n7,n7)
| n3 != sum(n9,n5)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1499,plain,
( n8 != sK1
| n7 != pred(n8)
| n8 != sK0
| succ(n8) != n9
| n5 != sum(n7,n9)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1500,plain,
( n7 != sum(n8,n10)
| n5 != sum(n7,n9)
| n8 != pred(n9)
| succ(n8) != n9
| n6 != sum(n8,n9)
| n8 != sK1
| n7 != pred(n8)
| n9 != sK0
| succ(n9) != n10
| n6 != sum(n7,n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n1 != sum(n6,n6)
| n1 != sum(n7,n5)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1501,plain,
( n8 != sum(n3,n5)
| n5 != sum(n7,n9)
| n3 != pred(n4)
| succ(n8) != n9
| n1 != sum(n3,n9)
| n8 != sK1
| n7 != pred(n8)
| n4 != sK0
| succ(n4) != n5
| n1 != sum(n7,n5)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n2 != sum(n1,n1)
| n2 != sum(n8,n5)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1502,plain,
( n4 != sum(n1,n3)
| n5 != sum(n7,n9)
| n1 != pred(n2)
| succ(n8) != n9
| n10 != sum(n1,n9)
| n8 != sK1
| n7 != pred(n8)
| n2 != sK0
| succ(n2) != n3
| n10 != sum(n7,n3)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n9 != sum(n10,n10)
| n9 != sum(n4,n5)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1503,plain,
( n4 != sum(n1,n3)
| n9 != sum(n9,n0)
| n1 != pred(n2)
| n0 != succ(n10)
| n1 != sum(n1,n0)
| n10 != sK1
| n9 != pred(n10)
| n2 != sK0
| succ(n2) != n3
| n1 != sum(n9,n3)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n2 != sum(n1,n1)
| n2 != sum(n4,n9)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1504,plain,
( n7 != sum(n8,n10)
| n9 != sum(n9,n0)
| n8 != pred(n9)
| n0 != succ(n10)
| n8 != sum(n8,n0)
| n10 != sK1
| n9 != pred(n10)
| n9 != sK0
| succ(n9) != n10
| n8 != sum(n9,n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n5 != sum(n8,n8)
| n5 != sum(n7,n9)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1505,plain,
( n0 != sum(n10,n1)
| n9 != sum(n9,n0)
| n10 != pred(n0)
| n0 != succ(n10)
| n10 != sum(n10,n0)
| n10 != sK1
| n9 != pred(n10)
| n0 != sK0
| succ(n0) != n1
| n10 != sum(n9,n1)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n9 != sum(n10,n10)
| n9 != sum(n0,n9)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1506,plain,
( n1 != sum(n5,n7)
| n9 != sum(n9,n0)
| n5 != pred(n6)
| n0 != succ(n10)
| n5 != sum(n5,n0)
| n10 != sK1
| n9 != pred(n10)
| n6 != sK0
| succ(n6) != n7
| n5 != sum(n9,n7)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n10 != sum(n5,n5)
| n10 != sum(n1,n9)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1507,plain,
( n3 != sum(n6,n8)
| n9 != sum(n9,n0)
| n6 != pred(n7)
| n0 != succ(n10)
| n6 != sum(n6,n0)
| n10 != sK1
| n9 != pred(n10)
| n7 != sK0
| succ(n7) != n8
| n6 != sum(n9,n8)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n1 != sum(n6,n6)
| n1 != sum(n3,n9)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1508,plain,
( n5 != sum(n7,n9)
| n9 != sum(n9,n0)
| n7 != pred(n8)
| n0 != succ(n10)
| n7 != sum(n7,n0)
| n10 != sK1
| n9 != pred(n10)
| n8 != sK0
| succ(n8) != n9
| n7 != sum(n9,n9)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n3 != sum(n7,n7)
| n3 != sum(n5,n9)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1509,plain,
( n10 != sK1
| n9 != pred(n10)
| n10 != sK0
| n0 != succ(n10)
| n9 != sum(n9,n0)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1510,plain,
( n8 != sum(n3,n5)
| n9 != sum(n9,n0)
| n3 != pred(n4)
| n0 != succ(n10)
| n3 != sum(n3,n0)
| n10 != sK1
| n9 != pred(n10)
| n4 != sK0
| succ(n4) != n5
| n3 != sum(n9,n5)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n6 != sum(n3,n3)
| n6 != sum(n8,n9)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1511,plain,
( n6 != sum(n2,n4)
| n9 != sum(n9,n0)
| n2 != pred(n3)
| n0 != succ(n10)
| n2 != sum(n2,n0)
| n10 != sK1
| n9 != pred(n10)
| n3 != sK0
| succ(n3) != n4
| n2 != sum(n9,n4)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n4 != sum(n2,n2)
| n4 != sum(n6,n9)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1512,plain,
( n2 != sum(n0,n2)
| n9 != sum(n9,n0)
| n0 != pred(n1)
| n0 != succ(n10)
| n10 != sK1
| n9 != pred(n10)
| n1 != sK0
| succ(n1) != n2
| n0 != sum(n9,n2)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n0 != sum(n0,n0)
| n0 != sum(n2,n9)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1513,plain,
( n4 != sum(n1,n3)
| n1 != sum(n5,n7)
| n1 != pred(n2)
| succ(n6) != n7
| n8 != sum(n1,n7)
| n6 != sK1
| n5 != pred(n6)
| n2 != sK0
| succ(n2) != n3
| n8 != sum(n5,n3)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n5 != sum(n8,n8)
| n5 != sum(n4,n1)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1514,plain,
( n4 != sum(n1,n3)
| n8 != sum(n3,n5)
| n1 != pred(n2)
| succ(n4) != n5
| n6 != sum(n1,n5)
| n4 != sK1
| n3 != pred(n4)
| n2 != sK0
| succ(n2) != n3
| n6 != sum(n3,n3)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n1 != sum(n6,n6)
| n1 != sum(n4,n8)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1515,plain,
( n4 != sum(n1,n3)
| n3 != sum(n6,n8)
| n1 != pred(n2)
| succ(n7) != n8
| n9 != sum(n1,n8)
| n7 != sK1
| n6 != pred(n7)
| n2 != sK0
| succ(n2) != n3
| n9 != sum(n6,n3)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n7 != sum(n9,n9)
| n7 != sum(n4,n3)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1516,plain,
( n4 != sum(n1,n3)
| n6 != sum(n2,n4)
| n1 != pred(n2)
| succ(n3) != n4
| n5 != sum(n1,n4)
| n3 != sK1
| n2 != pred(n3)
| n2 != sK0
| succ(n2) != n3
| n5 != sum(n2,n3)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n10 != sum(n5,n5)
| n10 != sum(n4,n6)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1517,plain,
( n4 != sum(n1,n3)
| n7 != sum(n8,n10)
| n1 != pred(n2)
| succ(n9) != n10
| n0 != sum(n1,n10)
| n9 != sK1
| n8 != pred(n9)
| n2 != sK0
| succ(n2) != n3
| n0 != sum(n8,n3)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n0 != sum(n0,n0)
| n0 != sum(n4,n7)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1518,plain,
( n4 != sum(n1,n3)
| n2 != sum(n0,n2)
| n1 != pred(n2)
| succ(n1) != n2
| n3 != sum(n1,n2)
| n1 != sK1
| n0 != pred(n1)
| n2 != sK0
| succ(n2) != n3
| n3 != sum(n0,n3)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n6 != sum(n3,n3)
| n6 != sum(n4,n2)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1519,plain,
( n4 != sum(n1,n3)
| n10 != sum(n4,n6)
| n1 != pred(n2)
| succ(n5) != n6
| n7 != sum(n1,n6)
| n5 != sK1
| n4 != pred(n5)
| n2 != sK0
| succ(n2) != n3
| n7 != sum(n4,n3)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n3 != sum(n7,n7)
| n3 != sum(n4,n10)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1520,plain,
( n2 != sK1
| n1 != pred(n2)
| n2 != sK0
| succ(n2) != n3
| n4 != sum(n1,n3)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1521,plain,
( n6 != sum(n2,n4)
| n2 != sum(n0,n2)
| n2 != pred(n3)
| succ(n1) != n2
| n4 != sum(n2,n2)
| n1 != sK1
| n0 != pred(n1)
| n3 != sK0
| succ(n3) != n4
| n4 != sum(n0,n4)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n8 != sum(n4,n4)
| n8 != sum(n6,n2)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1522,plain,
( n3 != sum(n6,n8)
| n2 != sum(n0,n2)
| n6 != pred(n7)
| succ(n1) != n2
| n8 != sum(n6,n2)
| n1 != sK1
| n0 != pred(n1)
| n7 != sK0
| succ(n7) != n8
| n8 != sum(n0,n8)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n5 != sum(n8,n8)
| n5 != sum(n3,n2)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1523,plain,
( n1 != sK1
| n0 != pred(n1)
| n1 != sK0
| succ(n1) != n2
| n2 != sum(n0,n2)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1524,plain,
( n8 != sum(n3,n5)
| n2 != sum(n0,n2)
| n3 != pred(n4)
| succ(n1) != n2
| n5 != sum(n3,n2)
| n1 != sK1
| n0 != pred(n1)
| n4 != sK0
| succ(n4) != n5
| n5 != sum(n0,n5)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n10 != sum(n5,n5)
| n10 != sum(n8,n2)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1525,plain,
( n1 != sum(n5,n7)
| n2 != sum(n0,n2)
| n5 != pred(n6)
| succ(n1) != n2
| n7 != sum(n5,n2)
| n1 != sK1
| n0 != pred(n1)
| n6 != sK0
| succ(n6) != n7
| n7 != sum(n0,n7)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n3 != sum(n7,n7)
| n3 != sum(n1,n2)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1526,plain,
( n0 != sum(n10,n1)
| n10 != pred(n0)
| succ(n1) != n2
| n1 != sum(n10,n2)
| n1 != sK1
| n0 != pred(n1)
| n0 != sK0
| succ(n0) != n1
| n1 != sum(n0,n1)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n2 != sum(n1,n1)
| n2 != sum(n0,n2)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1527,plain,
( n7 != sum(n8,n10)
| n2 != sum(n0,n2)
| n8 != pred(n9)
| succ(n1) != n2
| n10 != sum(n8,n2)
| n1 != sK1
| n0 != pred(n1)
| n9 != sK0
| succ(n9) != n10
| n10 != sum(n0,n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n9 != sum(n10,n10)
| n9 != sum(n7,n2)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1528,plain,
( n9 != sum(n9,n0)
| n2 != sum(n0,n2)
| n0 != pred(n1)
| n9 != pred(n10)
| n1 != sK1
| succ(n1) != n2
| n10 != sK0
| n0 != succ(n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n0 != sum(n0,n0)
| n0 != sum(n9,n2)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1529,plain,
( n5 != sum(n7,n9)
| n2 != sum(n0,n2)
| n7 != pred(n8)
| succ(n1) != n2
| n9 != sum(n7,n2)
| n1 != sK1
| n0 != pred(n1)
| n8 != sK0
| succ(n8) != n9
| n9 != sum(n0,n9)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n7 != sum(n9,n9)
| n7 != sum(n5,n2)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1530,plain,
( n7 != sum(n8,n10)
| n3 != sum(n6,n8)
| n8 != pred(n9)
| succ(n7) != n8
| n5 != sum(n8,n8)
| n7 != sK1
| n6 != pred(n7)
| n9 != sK0
| succ(n9) != n10
| n5 != sum(n6,n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n10 != sum(n5,n5)
| n10 != sum(n7,n3)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1531,plain,
( n7 != sum(n8,n10)
| n8 != sum(n3,n5)
| n8 != pred(n9)
| succ(n4) != n5
| n2 != sum(n8,n5)
| n4 != sK1
| n3 != pred(n4)
| n9 != sK0
| succ(n9) != n10
| n2 != sum(n3,n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n4 != sum(n2,n2)
| n4 != sum(n7,n8)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1532,plain,
( n7 != sum(n8,n10)
| n1 != sum(n5,n7)
| n8 != pred(n9)
| succ(n6) != n7
| n4 != sum(n8,n7)
| n6 != sK1
| n5 != pred(n6)
| n9 != sK0
| succ(n9) != n10
| n4 != sum(n5,n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n8 != sum(n4,n4)
| n8 != sum(n7,n1)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1533,plain,
( n7 != sum(n8,n10)
| n10 != sum(n4,n6)
| n8 != pred(n9)
| succ(n5) != n6
| n3 != sum(n8,n6)
| n5 != sK1
| n4 != pred(n5)
| n9 != sK0
| succ(n9) != n10
| n3 != sum(n4,n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n6 != sum(n3,n3)
| n6 != sum(n7,n10)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1534,plain,
( n9 != sK1
| n8 != pred(n9)
| n9 != sK0
| succ(n9) != n10
| n7 != sum(n8,n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1535,plain,
( n7 != sum(n8,n10)
| n6 != sum(n2,n4)
| n8 != pred(n9)
| succ(n3) != n4
| n1 != sum(n8,n4)
| n3 != sK1
| n2 != pred(n3)
| n9 != sK0
| succ(n9) != n10
| n1 != sum(n2,n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n2 != sum(n1,n1)
| n2 != sum(n7,n6)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1536,plain,
( n7 != sum(n8,n10)
| n0 != sum(n10,n1)
| n8 != pred(n9)
| succ(n0) != n1
| n9 != sum(n8,n1)
| n0 != sK1
| n10 != pred(n0)
| n9 != sK0
| succ(n9) != n10
| n9 != sum(n10,n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n7 != sum(n9,n9)
| n7 != sum(n7,n0)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1537,plain,
( n7 != sum(n8,n10)
| n4 != sum(n1,n3)
| n8 != pred(n9)
| succ(n2) != n3
| n0 != sum(n8,n3)
| n2 != sK1
| n1 != pred(n2)
| n9 != sK0
| succ(n9) != n10
| n0 != sum(n1,n10)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n0 != sum(n0,n0)
| n0 != sum(n7,n4)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1538,plain,
( n5 != sum(n7,n9)
| n10 != sum(n4,n6)
| n7 != pred(n8)
| succ(n5) != n6
| n2 != sum(n7,n6)
| n5 != sK1
| n4 != pred(n5)
| n8 != sK0
| succ(n8) != n9
| n2 != sum(n4,n9)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n4 != sum(n2,n2)
| n4 != sum(n5,n10)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1539,plain,
( n0 != sum(n10,n1)
| n10 != sum(n4,n6)
| n10 != pred(n0)
| succ(n5) != n6
| n5 != sum(n10,n6)
| n5 != sK1
| n4 != pred(n5)
| n0 != sK0
| succ(n0) != n1
| n5 != sum(n4,n1)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n10 != sum(n5,n5)
| n10 != sum(n0,n10)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1540,plain,
( n8 != sum(n3,n5)
| n10 != sum(n4,n6)
| n3 != pred(n4)
| succ(n5) != n6
| n9 != sum(n3,n6)
| n5 != sK1
| n4 != pred(n5)
| n4 != sK0
| succ(n4) != n5
| n9 != sum(n4,n5)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n7 != sum(n9,n9)
| n7 != sum(n8,n10)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1541,plain,
( n2 != sum(n0,n2)
| n10 != sum(n4,n6)
| n0 != pred(n1)
| succ(n5) != n6
| n6 != sum(n0,n6)
| n5 != sK1
| n4 != pred(n5)
| n1 != sK0
| succ(n1) != n2
| n6 != sum(n4,n2)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n1 != sum(n6,n6)
| n1 != sum(n2,n10)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1542,plain,
( n9 != sum(n9,n0)
| n10 != sum(n4,n6)
| n9 != pred(n10)
| succ(n5) != n6
| n4 != sum(n9,n6)
| n5 != sK1
| n4 != pred(n5)
| n10 != sK0
| n0 != succ(n10)
| n4 != sum(n4,n0)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n8 != sum(n4,n4)
| n8 != sum(n9,n10)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1543,plain,
( n6 != sum(n2,n4)
| n10 != sum(n4,n6)
| n2 != pred(n3)
| succ(n5) != n6
| n8 != sum(n2,n6)
| n5 != sK1
| n4 != pred(n5)
| n3 != sK0
| succ(n3) != n4
| n8 != sum(n4,n4)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n5 != sum(n8,n8)
| n5 != sum(n6,n10)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1544,plain,
( n3 != sum(n6,n8)
| n10 != sum(n4,n6)
| n6 != pred(n7)
| succ(n5) != n6
| n1 != sum(n6,n6)
| n5 != sK1
| n4 != pred(n5)
| n7 != sK0
| succ(n7) != n8
| n1 != sum(n4,n8)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n2 != sum(n1,n1)
| n2 != sum(n3,n10)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1545,plain,
( n1 != sum(n5,n7)
| n10 != sum(n4,n6)
| n5 != pred(n6)
| succ(n5) != n6
| n0 != sum(n5,n6)
| n5 != sK1
| n4 != pred(n5)
| n6 != sK0
| succ(n6) != n7
| n0 != sum(n4,n7)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n0 != sum(n0,n0)
| n0 != sum(n1,n10)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1546,plain,
( n0 != sum(n10,n1)
| n8 != sum(n3,n5)
| n10 != pred(n0)
| succ(n4) != n5
| n4 != sum(n10,n5)
| n4 != sK1
| n3 != pred(n4)
| n0 != sK0
| succ(n0) != n1
| n4 != sum(n3,n1)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n8 != sum(n4,n4)
| n8 != sum(n0,n8)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1547,plain,
( n0 != sum(n10,n1)
| n1 != sum(n5,n7)
| n10 != pred(n0)
| succ(n6) != n7
| n6 != sum(n10,n7)
| n6 != sK1
| n5 != pred(n6)
| n0 != sK0
| succ(n0) != n1
| n6 != sum(n5,n1)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n1 != sum(n6,n6)
| n1 != sum(n0,n1)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1548,plain,
( n0 != sum(n10,n1)
| n7 != sum(n8,n10)
| n10 != pred(n0)
| succ(n9) != n10
| n9 != sum(n10,n10)
| n9 != sK1
| n8 != pred(n9)
| n0 != sK0
| succ(n0) != n1
| n9 != sum(n8,n1)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n7 != sum(n9,n9)
| n7 != sum(n0,n7)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1549,plain,
( n0 != sum(n10,n1)
| n6 != sum(n2,n4)
| n10 != pred(n0)
| succ(n3) != n4
| n3 != sum(n10,n4)
| n3 != sK1
| n2 != pred(n3)
| n0 != sK0
| succ(n0) != n1
| n3 != sum(n2,n1)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n6 != sum(n3,n3)
| n6 != sum(n0,n6)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1550,plain,
( n0 != sum(n10,n1)
| n4 != sum(n1,n3)
| n10 != pred(n0)
| succ(n2) != n3
| n2 != sum(n10,n3)
| n2 != sK1
| n1 != pred(n2)
| n0 != sK0
| succ(n0) != n1
| n2 != sum(n1,n1)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n4 != sum(n2,n2)
| n4 != sum(n0,n4)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1551,plain,
( n0 != sum(n10,n1)
| n3 != sum(n6,n8)
| n10 != pred(n0)
| succ(n7) != n8
| n7 != sum(n10,n8)
| n7 != sK1
| n6 != pred(n7)
| n0 != sK0
| succ(n0) != n1
| n7 != sum(n6,n1)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n3 != sum(n7,n7)
| n3 != sum(n0,n3)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1552,plain,
( n9 != sum(n9,n0)
| n6 != sum(n2,n4)
| n9 != pred(n10)
| succ(n3) != n4
| n2 != sum(n9,n4)
| n3 != sK1
| n2 != pred(n3)
| n10 != sK0
| n0 != succ(n10)
| n2 != sum(n2,n0)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n4 != sum(n2,n2)
| n4 != sum(n9,n6)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1553,plain,
( n2 != sum(n0,n2)
| n6 != sum(n2,n4)
| n0 != pred(n1)
| succ(n3) != n4
| n4 != sum(n0,n4)
| n3 != sK1
| n2 != pred(n3)
| n1 != sK0
| succ(n1) != n2
| n4 != sum(n2,n2)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n8 != sum(n4,n4)
| n8 != sum(n2,n6)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1554,plain,
( n1 != sum(n5,n7)
| n6 != sum(n2,n4)
| n5 != pred(n6)
| succ(n3) != n4
| n9 != sum(n5,n4)
| n3 != sK1
| n2 != pred(n3)
| n6 != sK0
| succ(n6) != n7
| n9 != sum(n2,n7)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n7 != sum(n9,n9)
| n7 != sum(n1,n6)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1555,plain,
( n3 != sum(n6,n8)
| n6 != sum(n2,n4)
| n6 != pred(n7)
| succ(n3) != n4
| n10 != sum(n6,n4)
| n3 != sK1
| n2 != pred(n3)
| n7 != sK0
| succ(n7) != n8
| n10 != sum(n2,n8)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n9 != sum(n10,n10)
| n9 != sum(n3,n6)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1556,plain,
( n8 != sum(n3,n5)
| n6 != sum(n2,n4)
| n3 != pred(n4)
| succ(n3) != n4
| n7 != sum(n3,n4)
| n3 != sK1
| n2 != pred(n3)
| n4 != sK0
| succ(n4) != n5
| n7 != sum(n2,n5)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n3 != sum(n7,n7)
| n3 != sum(n8,n6)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1557,plain,
( n5 != sum(n7,n9)
| n6 != sum(n2,n4)
| n7 != pred(n8)
| succ(n3) != n4
| n0 != sum(n7,n4)
| n3 != sK1
| n2 != pred(n3)
| n8 != sK0
| succ(n8) != n9
| n0 != sum(n2,n9)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n0 != sum(n0,n0)
| n0 != sum(n5,n6)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1558,plain,
( n3 != sK1
| n2 != pred(n3)
| n3 != sK0
| succ(n3) != n4
| n6 != sum(n2,n4)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1559,plain,
( n7 != sK1
| n6 != pred(n7)
| n7 != sK0
| succ(n7) != n8
| n3 != sum(n6,n8)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1560,plain,
( n3 != sum(n6,n8)
| n4 != sum(n1,n3)
| n6 != pred(n7)
| succ(n2) != n3
| n9 != sum(n6,n3)
| n2 != sK1
| n1 != pred(n2)
| n7 != sK0
| succ(n7) != n8
| n9 != sum(n1,n8)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n7 != sum(n9,n9)
| n7 != sum(n3,n4)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1561,plain,
( n3 != sum(n6,n8)
| n0 != sum(n10,n1)
| n6 != pred(n7)
| succ(n0) != n1
| n7 != sum(n6,n1)
| n0 != sK1
| n10 != pred(n0)
| n7 != sK0
| succ(n7) != n8
| n7 != sum(n10,n8)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n3 != sum(n7,n7)
| n3 != sum(n3,n0)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1562,plain,
( n3 != sum(n6,n8)
| n8 != sum(n3,n5)
| n6 != pred(n7)
| succ(n4) != n5
| n0 != sum(n6,n5)
| n4 != sK1
| n3 != pred(n4)
| n7 != sK0
| succ(n7) != n8
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n0 != sum(n0,n0)
| n0 != sum(n3,n8)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1563,plain,
( n3 != sum(n6,n8)
| n1 != sum(n5,n7)
| n6 != pred(n7)
| succ(n6) != n7
| n2 != sum(n6,n7)
| n6 != sK1
| n5 != pred(n6)
| n7 != sK0
| succ(n7) != n8
| n2 != sum(n5,n8)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n4 != sum(n2,n2)
| n4 != sum(n3,n1)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1564,plain,
( n3 != sum(n6,n8)
| n7 != sum(n8,n10)
| n6 != pred(n7)
| succ(n9) != n10
| n5 != sum(n6,n10)
| n9 != sK1
| n8 != pred(n9)
| n7 != sK0
| succ(n7) != n8
| n5 != sum(n8,n8)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n10 != sum(n5,n5)
| n10 != sum(n3,n7)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1565,plain,
( n1 != sum(n5,n7)
| n8 != sum(n3,n5)
| n5 != pred(n6)
| succ(n4) != n5
| n10 != sum(n5,n5)
| n4 != sK1
| n3 != pred(n4)
| n6 != sK0
| succ(n6) != n7
| n10 != sum(n3,n7)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n9 != sum(n10,n10)
| n9 != sum(n1,n8)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1566,plain,
( n5 != sum(n7,n9)
| n8 != sum(n3,n5)
| n7 != pred(n8)
| succ(n4) != n5
| n1 != sum(n7,n5)
| n4 != sK1
| n3 != pred(n4)
| n8 != sK0
| succ(n8) != n9
| n1 != sum(n3,n9)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n2 != sum(n1,n1)
| n2 != sum(n5,n8)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1567,plain,
( n2 != sum(n0,n2)
| n8 != sum(n3,n5)
| n0 != pred(n1)
| succ(n4) != n5
| n5 != sum(n0,n5)
| n4 != sK1
| n3 != pred(n4)
| n1 != sK0
| succ(n1) != n2
| n5 != sum(n3,n2)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n10 != sum(n5,n5)
| n10 != sum(n2,n8)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1568,plain,
( n6 != sum(n2,n4)
| n8 != sum(n3,n5)
| n2 != pred(n3)
| succ(n4) != n5
| n7 != sum(n2,n5)
| n4 != sK1
| n3 != pred(n4)
| n3 != sK0
| succ(n3) != n4
| n7 != sum(n3,n4)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n3 != sum(n7,n7)
| n3 != sum(n6,n8)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1569,plain,
( n4 != sK1
| n3 != pred(n4)
| n4 != sK0
| succ(n4) != n5
| n8 != sum(n3,n5)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1570,plain,
( n9 != sum(n9,n0)
| n8 != sum(n3,n5)
| n9 != pred(n10)
| succ(n4) != n5
| n3 != sum(n9,n5)
| n4 != sK1
| n3 != pred(n4)
| n10 != sK0
| n0 != succ(n10)
| n3 != sum(n3,n0)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n6 != sum(n3,n3)
| n6 != sum(n9,n8)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1571,plain,
( n2 != sum(n0,n2)
| n3 != sum(n6,n8)
| n0 != pred(n1)
| succ(n7) != n8
| n8 != sum(n0,n8)
| n7 != sK1
| n6 != pred(n7)
| n1 != sK0
| succ(n1) != n2
| n8 != sum(n6,n2)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n5 != sum(n8,n8)
| n5 != sum(n2,n3)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1572,plain,
( n2 != sum(n0,n2)
| n1 != sum(n5,n7)
| n0 != pred(n1)
| succ(n6) != n7
| n7 != sum(n0,n7)
| n6 != sK1
| n5 != pred(n6)
| n1 != sK0
| succ(n1) != n2
| n7 != sum(n5,n2)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n3 != sum(n7,n7)
| n3 != sum(n2,n1)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1573,plain,
( n2 != sum(n0,n2)
| n7 != sum(n8,n10)
| n0 != pred(n1)
| succ(n9) != n10
| n10 != sum(n0,n10)
| n9 != sK1
| n8 != pred(n9)
| n1 != sK0
| succ(n1) != n2
| n10 != sum(n8,n2)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n9 != sum(n10,n10)
| n9 != sum(n2,n7)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1574,plain,
( n2 != sum(n0,n2)
| n4 != sum(n1,n3)
| n0 != pred(n1)
| succ(n2) != n3
| n3 != sum(n0,n3)
| n2 != sK1
| n1 != pred(n2)
| n1 != sK0
| succ(n1) != n2
| n3 != sum(n1,n2)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n6 != sum(n3,n3)
| n6 != sum(n2,n4)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1575,plain,
( n1 != sum(n5,n7)
| n3 != sum(n6,n8)
| n5 != pred(n6)
| succ(n7) != n8
| n2 != sum(n5,n8)
| n7 != sK1
| n6 != pred(n7)
| n6 != sK0
| succ(n6) != n7
| n2 != sum(n6,n7)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n4 != sum(n2,n2)
| n4 != sum(n1,n3)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1576,plain,
( n8 != sum(n3,n5)
| n3 != sum(n6,n8)
| n3 != pred(n4)
| succ(n7) != n8
| n0 != sum(n3,n8)
| n7 != sK1
| n6 != pred(n7)
| n4 != sK0
| succ(n4) != n5
| n0 != sum(n6,n5)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n0 != sum(n0,n0)
| n0 != sum(n8,n3)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1577,plain,
( n6 != sum(n2,n4)
| n3 != sum(n6,n8)
| n2 != pred(n3)
| succ(n7) != n8
| n10 != sum(n2,n8)
| n7 != sK1
| n6 != pred(n7)
| n3 != sK0
| succ(n3) != n4
| n10 != sum(n6,n4)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n9 != sum(n10,n10)
| n9 != sum(n6,n3)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1578,plain,
( n5 != sum(n7,n9)
| n3 != sum(n6,n8)
| n7 != pred(n8)
| succ(n7) != n8
| n4 != sum(n7,n8)
| n7 != sK1
| n6 != pred(n7)
| n8 != sK0
| succ(n8) != n9
| n4 != sum(n6,n9)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n8 != sum(n4,n4)
| n8 != sum(n5,n3)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1579,plain,
( n9 != sum(n9,n0)
| n3 != sum(n6,n8)
| n9 != pred(n10)
| succ(n7) != n8
| n6 != sum(n9,n8)
| n7 != sK1
| n6 != pred(n7)
| n10 != sK0
| n0 != succ(n10)
| n6 != sum(n6,n0)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n1 != sum(n6,n6)
| n1 != sum(n9,n3)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1580,plain,
( n6 != sum(n2,n4)
| n7 != sum(n8,n10)
| n2 != pred(n3)
| succ(n9) != n10
| n1 != sum(n2,n10)
| n9 != sK1
| n8 != pred(n9)
| n3 != sK0
| succ(n3) != n4
| n1 != sum(n8,n4)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n2 != sum(n1,n1)
| n2 != sum(n6,n7)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1581,plain,
( n6 != sum(n2,n4)
| n1 != sum(n5,n7)
| n2 != pred(n3)
| succ(n6) != n7
| n9 != sum(n2,n7)
| n6 != sK1
| n5 != pred(n6)
| n3 != sK0
| succ(n3) != n4
| n9 != sum(n5,n4)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n7 != sum(n9,n9)
| n7 != sum(n6,n1)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1582,plain,
( n6 != sum(n2,n4)
| n4 != sum(n1,n3)
| n2 != pred(n3)
| succ(n2) != n3
| n5 != sum(n2,n3)
| n2 != sK1
| n1 != pred(n2)
| n3 != sK0
| succ(n3) != n4
| n5 != sum(n1,n4)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n10 != sum(n5,n5)
| n10 != sum(n6,n4)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1583,plain,
( n1 != sum(n5,n7)
| n4 != sum(n1,n3)
| n5 != pred(n6)
| succ(n2) != n3
| n8 != sum(n5,n3)
| n2 != sK1
| n1 != pred(n2)
| n6 != sK0
| succ(n6) != n7
| n8 != sum(n1,n7)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n5 != sum(n8,n8)
| n5 != sum(n1,n4)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1584,plain,
( n8 != sum(n3,n5)
| n4 != sum(n1,n3)
| n3 != pred(n4)
| succ(n2) != n3
| n6 != sum(n3,n3)
| n2 != sK1
| n1 != pred(n2)
| n4 != sK0
| succ(n4) != n5
| n6 != sum(n1,n5)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n1 != sum(n6,n6)
| n1 != sum(n8,n4)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1585,plain,
( n9 != sum(n9,n0)
| n4 != sum(n1,n3)
| n9 != pred(n10)
| succ(n2) != n3
| n1 != sum(n9,n3)
| n2 != sK1
| n1 != pred(n2)
| n10 != sK0
| n0 != succ(n10)
| n1 != sum(n1,n0)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n2 != sum(n1,n1)
| n2 != sum(n9,n4)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1586,plain,
( n5 != sum(n7,n9)
| n4 != sum(n1,n3)
| n7 != pred(n8)
| succ(n2) != n3
| n10 != sum(n7,n3)
| n2 != sK1
| n1 != pred(n2)
| n8 != sK0
| succ(n8) != n9
| n10 != sum(n1,n9)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n9 != sum(n10,n10)
| n9 != sum(n5,n4)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1587,plain,
( n8 != sum(n3,n5)
| n1 != sum(n5,n7)
| n3 != pred(n4)
| succ(n6) != n7
| n10 != sum(n3,n7)
| n6 != sK1
| n5 != pred(n6)
| n4 != sK0
| succ(n4) != n5
| n10 != sum(n5,n5)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n9 != sum(n10,n10)
| n9 != sum(n8,n1)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1588,plain,
( n8 != sum(n3,n5)
| n7 != sum(n8,n10)
| n3 != pred(n4)
| succ(n9) != n10
| n2 != sum(n3,n10)
| n9 != sK1
| n8 != pred(n9)
| n4 != sK0
| succ(n4) != n5
| n2 != sum(n8,n5)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n4 != sum(n2,n2)
| n4 != sum(n8,n7)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1589,plain,
( n1 != sum(n5,n7)
| n0 != sum(n10,n1)
| n5 != pred(n6)
| succ(n0) != n1
| n6 != sum(n5,n1)
| n0 != sK1
| n10 != pred(n0)
| n6 != sK0
| succ(n6) != n7
| n6 != sum(n10,n7)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n1 != sum(n6,n6)
| n1 != sum(n1,n0)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1590,plain,
( n0 != sum(n10,n1)
| n9 != pred(n10)
| succ(n0) != n1
| n10 != sum(n9,n1)
| n0 != sK1
| n10 != pred(n0)
| n10 != sK0
| n0 != succ(n10)
| n10 != sum(n10,n0)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n9 != sum(n10,n10)
| n9 != sum(n9,n0)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1591,plain,
( n5 != sum(n7,n9)
| n0 != sum(n10,n1)
| n7 != pred(n8)
| succ(n0) != n1
| n8 != sum(n7,n1)
| n0 != sK1
| n10 != pred(n0)
| n8 != sK0
| succ(n8) != n9
| n8 != sum(n10,n9)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n5 != sum(n8,n8)
| n5 != sum(n5,n0)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1592,plain,
( n6 != sK1
| n5 != pred(n6)
| n6 != sK0
| succ(n6) != n7
| n1 != sum(n5,n7)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1593,plain,
( n1 != sum(n5,n7)
| n7 != sum(n8,n10)
| n5 != pred(n6)
| succ(n9) != n10
| n4 != sum(n5,n10)
| n9 != sK1
| n8 != pred(n9)
| n6 != sK0
| succ(n6) != n7
| n4 != sum(n8,n7)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n8 != sum(n4,n4)
| n8 != sum(n1,n7)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1594,plain,
( n5 != sum(n7,n9)
| n7 != sum(n8,n10)
| n7 != pred(n8)
| succ(n9) != n10
| n6 != sum(n7,n10)
| n9 != sK1
| n8 != pred(n9)
| n8 != sK0
| succ(n8) != n9
| n6 != sum(n8,n9)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n1 != sum(n6,n6)
| n1 != sum(n5,n7)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1595,plain,
( n9 != sum(n9,n0)
| n7 != sum(n8,n10)
| n9 != pred(n10)
| succ(n9) != n10
| n8 != sum(n9,n10)
| n9 != sK1
| n8 != pred(n9)
| n10 != sK0
| n0 != succ(n10)
| n8 != sum(n8,n0)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n5 != sum(n8,n8)
| n5 != sum(n9,n7)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1596,plain,
( n5 != sum(n7,n9)
| n1 != sum(n5,n7)
| n7 != pred(n8)
| succ(n6) != n7
| n3 != sum(n7,n7)
| n6 != sK1
| n5 != pred(n6)
| n8 != sK0
| succ(n8) != n9
| n3 != sum(n5,n9)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n6 != sum(n3,n3)
| n6 != sum(n5,n1)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1597,plain,
( n9 != sum(n9,n0)
| n1 != sum(n5,n7)
| n9 != pred(n10)
| succ(n6) != n7
| n5 != sum(n9,n7)
| n6 != sK1
| n5 != pred(n6)
| n10 != sK0
| n0 != succ(n10)
| n5 != sum(n5,n0)
| sK2 != sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
| sK3 != sum(sum(pred(sK0),succ(sK0)),sum(pred(sK1),succ(sK1)))
| n10 != sum(n5,n5)
| n10 != sum(n9,n1)
| sK2 = sK3 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s56,plain,
spl22_56,
inference(sat_conversion,[],[f502]) ).
cnf(s57,plain,
spl22_57,
inference(sat_conversion,[],[f507]) ).
cnf(s58,plain,
spl22_58,
inference(sat_conversion,[],[f512]) ).
cnf(s59,plain,
spl22_59,
inference(sat_conversion,[],[f517]) ).
cnf(s60,plain,
spl22_60,
inference(sat_conversion,[],[f522]) ).
cnf(s61,plain,
spl22_61,
inference(sat_conversion,[],[f527]) ).
cnf(s62,plain,
spl22_62,
inference(sat_conversion,[],[f532]) ).
cnf(s63,plain,
spl22_63,
inference(sat_conversion,[],[f537]) ).
cnf(s64,plain,
spl22_64,
inference(sat_conversion,[],[f542]) ).
cnf(s65,plain,
spl22_65,
inference(sat_conversion,[],[f547]) ).
cnf(s66,plain,
spl22_66,
inference(sat_conversion,[],[f552]) ).
cnf(s67,plain,
spl22_67,
inference(sat_conversion,[],[f557]) ).
cnf(s68,plain,
spl22_68,
inference(sat_conversion,[],[f562]) ).
cnf(s69,plain,
spl22_69,
inference(sat_conversion,[],[f567]) ).
cnf(s70,plain,
spl22_70,
inference(sat_conversion,[],[f572]) ).
cnf(s71,plain,
spl22_71,
inference(sat_conversion,[],[f577]) ).
cnf(s72,plain,
spl22_72,
inference(sat_conversion,[],[f582]) ).
cnf(s73,plain,
spl22_73,
inference(sat_conversion,[],[f587]) ).
cnf(s74,plain,
spl22_74,
inference(sat_conversion,[],[f592]) ).
cnf(s75,plain,
spl22_75,
inference(sat_conversion,[],[f597]) ).
cnf(s76,plain,
spl22_76,
inference(sat_conversion,[],[f602]) ).
cnf(s77,plain,
spl22_77,
inference(sat_conversion,[],[f607]) ).
cnf(s78,plain,
spl22_78,
inference(sat_conversion,[],[f612]) ).
cnf(s79,plain,
spl22_79,
inference(sat_conversion,[],[f617]) ).
cnf(s80,plain,
spl22_80,
inference(sat_conversion,[],[f622]) ).
cnf(s81,plain,
spl22_81,
inference(sat_conversion,[],[f627]) ).
cnf(s82,plain,
spl22_82,
inference(sat_conversion,[],[f632]) ).
cnf(s83,plain,
spl22_83,
inference(sat_conversion,[],[f637]) ).
cnf(s84,plain,
spl22_84,
inference(sat_conversion,[],[f642]) ).
cnf(s85,plain,
spl22_85,
inference(sat_conversion,[],[f647]) ).
cnf(s86,plain,
spl22_86,
inference(sat_conversion,[],[f652]) ).
cnf(s87,plain,
spl22_87,
inference(sat_conversion,[],[f657]) ).
cnf(s88,plain,
spl22_88,
inference(sat_conversion,[],[f662]) ).
cnf(s89,plain,
spl22_89,
inference(sat_conversion,[],[f667]) ).
cnf(s90,plain,
spl22_90,
inference(sat_conversion,[],[f672]) ).
cnf(s91,plain,
spl22_91,
inference(sat_conversion,[],[f677]) ).
cnf(s92,plain,
spl22_92,
inference(sat_conversion,[],[f682]) ).
cnf(s93,plain,
spl22_93,
inference(sat_conversion,[],[f687]) ).
cnf(s94,plain,
spl22_94,
inference(sat_conversion,[],[f692]) ).
cnf(s95,plain,
spl22_95,
inference(sat_conversion,[],[f697]) ).
cnf(s96,plain,
spl22_96,
inference(sat_conversion,[],[f702]) ).
cnf(s97,plain,
spl22_97,
inference(sat_conversion,[],[f707]) ).
cnf(s98,plain,
spl22_98,
inference(sat_conversion,[],[f712]) ).
cnf(s99,plain,
spl22_99,
inference(sat_conversion,[],[f717]) ).
cnf(s100,plain,
spl22_100,
inference(sat_conversion,[],[f722]) ).
cnf(s101,plain,
spl22_101,
inference(sat_conversion,[],[f727]) ).
cnf(s102,plain,
spl22_102,
inference(sat_conversion,[],[f732]) ).
cnf(s103,plain,
spl22_103,
inference(sat_conversion,[],[f737]) ).
cnf(s104,plain,
spl22_104,
inference(sat_conversion,[],[f742]) ).
cnf(s105,plain,
spl22_105,
inference(sat_conversion,[],[f747]) ).
cnf(s106,plain,
spl22_106,
inference(sat_conversion,[],[f752]) ).
cnf(s107,plain,
spl22_107,
inference(sat_conversion,[],[f757]) ).
cnf(s108,plain,
spl22_108,
inference(sat_conversion,[],[f762]) ).
cnf(s109,plain,
spl22_109,
inference(sat_conversion,[],[f767]) ).
cnf(s110,plain,
spl22_110,
inference(sat_conversion,[],[f772]) ).
cnf(s111,plain,
spl22_111,
inference(sat_conversion,[],[f777]) ).
cnf(s112,plain,
spl22_112,
inference(sat_conversion,[],[f782]) ).
cnf(s113,plain,
spl22_113,
inference(sat_conversion,[],[f787]) ).
cnf(s114,plain,
spl22_114,
inference(sat_conversion,[],[f792]) ).
cnf(s115,plain,
spl22_115,
inference(sat_conversion,[],[f797]) ).
cnf(s116,plain,
spl22_116,
inference(sat_conversion,[],[f802]) ).
cnf(s117,plain,
spl22_117,
inference(sat_conversion,[],[f807]) ).
cnf(s118,plain,
spl22_118,
inference(sat_conversion,[],[f812]) ).
cnf(s119,plain,
spl22_119,
inference(sat_conversion,[],[f817]) ).
cnf(s120,plain,
spl22_120,
inference(sat_conversion,[],[f822]) ).
cnf(s121,plain,
spl22_121,
inference(sat_conversion,[],[f827]) ).
cnf(s122,plain,
spl22_122,
inference(sat_conversion,[],[f832]) ).
cnf(s123,plain,
spl22_123,
inference(sat_conversion,[],[f837]) ).
cnf(s124,plain,
spl22_124,
inference(sat_conversion,[],[f842]) ).
cnf(s125,plain,
spl22_125,
inference(sat_conversion,[],[f847]) ).
cnf(s126,plain,
spl22_126,
inference(sat_conversion,[],[f852]) ).
cnf(s127,plain,
spl22_127,
inference(sat_conversion,[],[f857]) ).
cnf(s128,plain,
spl22_128,
inference(sat_conversion,[],[f862]) ).
cnf(s129,plain,
spl22_129,
inference(sat_conversion,[],[f867]) ).
cnf(s130,plain,
spl22_130,
inference(sat_conversion,[],[f872]) ).
cnf(s131,plain,
spl22_131,
inference(sat_conversion,[],[f877]) ).
cnf(s132,plain,
spl22_132,
inference(sat_conversion,[],[f882]) ).
cnf(s133,plain,
spl22_133,
inference(sat_conversion,[],[f887]) ).
cnf(s134,plain,
spl22_134,
inference(sat_conversion,[],[f892]) ).
cnf(s135,plain,
spl22_135,
inference(sat_conversion,[],[f897]) ).
cnf(s136,plain,
spl22_136,
inference(sat_conversion,[],[f902]) ).
cnf(s137,plain,
spl22_137,
inference(sat_conversion,[],[f907]) ).
cnf(s138,plain,
spl22_138,
inference(sat_conversion,[],[f912]) ).
cnf(s139,plain,
spl22_139,
inference(sat_conversion,[],[f917]) ).
cnf(s140,plain,
spl22_140,
inference(sat_conversion,[],[f922]) ).
cnf(s141,plain,
spl22_141,
inference(sat_conversion,[],[f927]) ).
cnf(s142,plain,
spl22_142,
inference(sat_conversion,[],[f932]) ).
cnf(s143,plain,
spl22_143,
inference(sat_conversion,[],[f937]) ).
cnf(s144,plain,
spl22_144,
inference(sat_conversion,[],[f942]) ).
cnf(s145,plain,
spl22_145,
inference(sat_conversion,[],[f947]) ).
cnf(s146,plain,
spl22_146,
inference(sat_conversion,[],[f952]) ).
cnf(s147,plain,
spl22_147,
inference(sat_conversion,[],[f957]) ).
cnf(s148,plain,
spl22_148,
inference(sat_conversion,[],[f962]) ).
cnf(s149,plain,
spl22_149,
inference(sat_conversion,[],[f967]) ).
cnf(s150,plain,
spl22_150,
inference(sat_conversion,[],[f972]) ).
cnf(s151,plain,
spl22_151,
inference(sat_conversion,[],[f977]) ).
cnf(s152,plain,
spl22_152,
inference(sat_conversion,[],[f982]) ).
cnf(s153,plain,
spl22_153,
inference(sat_conversion,[],[f987]) ).
cnf(s154,plain,
spl22_154,
inference(sat_conversion,[],[f992]) ).
cnf(s155,plain,
spl22_155,
inference(sat_conversion,[],[f997]) ).
cnf(s156,plain,
spl22_156,
inference(sat_conversion,[],[f1002]) ).
cnf(s157,plain,
spl22_157,
inference(sat_conversion,[],[f1007]) ).
cnf(s158,plain,
spl22_158,
inference(sat_conversion,[],[f1012]) ).
cnf(s159,plain,
spl22_159,
inference(sat_conversion,[],[f1017]) ).
cnf(s160,plain,
spl22_160,
inference(sat_conversion,[],[f1022]) ).
cnf(s161,plain,
spl22_161,
inference(sat_conversion,[],[f1027]) ).
cnf(s162,plain,
spl22_162,
inference(sat_conversion,[],[f1032]) ).
cnf(s163,plain,
spl22_163,
inference(sat_conversion,[],[f1037]) ).
cnf(s164,plain,
spl22_164,
inference(sat_conversion,[],[f1042]) ).
cnf(s165,plain,
spl22_165,
inference(sat_conversion,[],[f1047]) ).
cnf(s166,plain,
spl22_166,
inference(sat_conversion,[],[f1052]) ).
cnf(s167,plain,
spl22_167,
inference(sat_conversion,[],[f1057]) ).
cnf(s168,plain,
spl22_168,
inference(sat_conversion,[],[f1062]) ).
cnf(s169,plain,
spl22_169,
inference(sat_conversion,[],[f1067]) ).
cnf(s170,plain,
spl22_170,
inference(sat_conversion,[],[f1072]) ).
cnf(s171,plain,
spl22_171,
inference(sat_conversion,[],[f1077]) ).
cnf(s172,plain,
spl22_172,
inference(sat_conversion,[],[f1082]) ).
cnf(s173,plain,
spl22_173,
inference(sat_conversion,[],[f1087]) ).
cnf(s174,plain,
spl22_174,
inference(sat_conversion,[],[f1092]) ).
cnf(s175,plain,
spl22_175,
inference(sat_conversion,[],[f1097]) ).
cnf(s176,plain,
spl22_176,
inference(sat_conversion,[],[f1102]) ).
cnf(s177,plain,
spl22_177,
inference(sat_conversion,[],[f1107]) ).
cnf(s178,plain,
spl22_178,
inference(sat_conversion,[],[f1112]) ).
cnf(s179,plain,
spl22_179,
inference(sat_conversion,[],[f1117]) ).
cnf(s180,plain,
spl22_180,
inference(sat_conversion,[],[f1122]) ).
cnf(s181,plain,
spl22_181,
inference(sat_conversion,[],[f1127]) ).
cnf(s182,plain,
spl22_182,
inference(sat_conversion,[],[f1132]) ).
cnf(s183,plain,
spl22_183,
inference(sat_conversion,[],[f1137]) ).
cnf(s184,plain,
spl22_184,
inference(sat_conversion,[],[f1142]) ).
cnf(s185,plain,
spl22_185,
inference(sat_conversion,[],[f1147]) ).
cnf(s186,plain,
spl22_186,
inference(sat_conversion,[],[f1152]) ).
cnf(s187,plain,
spl22_187,
inference(sat_conversion,[],[f1157]) ).
cnf(s188,plain,
spl22_188,
inference(sat_conversion,[],[f1162]) ).
cnf(s189,plain,
spl22_189,
inference(sat_conversion,[],[f1167]) ).
cnf(s190,plain,
spl22_190,
inference(sat_conversion,[],[f1172]) ).
cnf(s191,plain,
spl22_191,
inference(sat_conversion,[],[f1177]) ).
cnf(s192,plain,
spl22_192,
inference(sat_conversion,[],[f1182]) ).
cnf(s193,plain,
spl22_193,
inference(sat_conversion,[],[f1187]) ).
cnf(s194,plain,
spl22_194,
inference(sat_conversion,[],[f1192]) ).
cnf(s195,plain,
spl22_195,
inference(sat_conversion,[],[f1197]) ).
cnf(s196,plain,
spl22_196,
inference(sat_conversion,[],[f1202]) ).
cnf(s197,plain,
spl22_197,
inference(sat_conversion,[],[f1207]) ).
cnf(s198,plain,
spl22_198,
inference(sat_conversion,[],[f1212]) ).
cnf(s199,plain,
spl22_199,
inference(sat_conversion,[],[f1217]) ).
cnf(s200,plain,
spl22_200,
inference(sat_conversion,[],[f1222]) ).
cnf(s201,plain,
spl22_201,
inference(sat_conversion,[],[f1227]) ).
cnf(s202,plain,
spl22_202,
inference(sat_conversion,[],[f1232]) ).
cnf(s203,plain,
spl22_203,
inference(sat_conversion,[],[f1237]) ).
cnf(s204,plain,
spl22_204,
inference(sat_conversion,[],[f1242]) ).
cnf(s205,plain,
spl22_205,
inference(sat_conversion,[],[f1247]) ).
cnf(s206,plain,
spl22_206,
inference(sat_conversion,[],[f1252]) ).
cnf(s207,plain,
spl22_207,
inference(sat_conversion,[],[f1257]) ).
cnf(s208,plain,
spl22_208,
inference(sat_conversion,[],[f1262]) ).
cnf(s209,plain,
spl22_209,
inference(sat_conversion,[],[f1267]) ).
cnf(s210,plain,
spl22_210,
inference(sat_conversion,[],[f1272]) ).
cnf(s211,plain,
spl22_211,
inference(sat_conversion,[],[f1277]) ).
cnf(s212,plain,
spl22_212,
inference(sat_conversion,[],[f1282]) ).
cnf(s213,plain,
spl22_213,
inference(sat_conversion,[],[f1287]) ).
cnf(s214,plain,
spl22_214,
inference(sat_conversion,[],[f1292]) ).
cnf(s215,plain,
spl22_215,
inference(sat_conversion,[],[f1297]) ).
cnf(s216,plain,
spl22_216,
inference(sat_conversion,[],[f1302]) ).
cnf(s217,plain,
spl22_217,
inference(sat_conversion,[],[f1307]) ).
cnf(s218,plain,
spl22_218,
inference(sat_conversion,[],[f1312]) ).
cnf(s219,plain,
( ~ spl22_219
| ~ spl22_220
| ~ spl22_221
| ~ spl22_222
| ~ spl22_223
| ~ spl22_224
| ~ spl22_225
| ~ spl22_226
| ~ spl22_227
| ~ spl22_228 ),
inference(sat_conversion,[],[f1353]) ).
cnf(s220,plain,
( spl22_229
| spl22_230
| spl22_231
| spl22_232
| spl22_233
| spl22_234
| spl22_235
| spl22_236
| spl22_237
| spl22_238
| spl22_239 ),
inference(sat_conversion,[],[f1398]) ).
cnf(s221,plain,
( spl22_240
| spl22_241
| spl22_242
| spl22_243
| spl22_244
| spl22_245
| spl22_246
| spl22_247
| spl22_248
| spl22_249
| spl22_250 ),
inference(sat_conversion,[],[f1443]) ).
cnf(s222,plain,
( ~ spl22_66
| ~ spl22_77
| ~ spl22_87
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_229
| ~ spl22_240 ),
inference(sat_conversion,[],[f1444]) ).
cnf(s223,plain,
( ~ spl22_199
| ~ spl22_200
| ~ spl22_201
| ~ spl22_202
| ~ spl22_203
| ~ spl22_204
| ~ spl22_205
| ~ spl22_206
| ~ spl22_207
| ~ spl22_208
| ~ spl22_209
| ~ spl22_210
| ~ spl22_211
| ~ spl22_212
| ~ spl22_213
| ~ spl22_214
| ~ spl22_215
| ~ spl22_216
| ~ spl22_219
| spl22_228 ),
inference(sat_conversion,[],[f1445]) ).
cnf(s224,plain,
( ~ spl22_215
| ~ spl22_216
| ~ spl22_219
| spl22_220 ),
inference(sat_conversion,[],[f1446]) ).
cnf(s225,plain,
( ~ spl22_65
| ~ spl22_66
| ~ spl22_76
| ~ spl22_77
| ~ spl22_86
| ~ spl22_87
| ~ spl22_176
| ~ spl22_186
| ~ spl22_196
| ~ spl22_197
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_230
| ~ spl22_240 ),
inference(sat_conversion,[],[f1447]) ).
cnf(s227,plain,
( ~ spl22_64
| ~ spl22_66
| ~ spl22_75
| ~ spl22_77
| ~ spl22_85
| ~ spl22_87
| ~ spl22_154
| ~ spl22_174
| ~ spl22_184
| ~ spl22_186
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_231
| ~ spl22_240 ),
inference(sat_conversion,[],[f1449]) ).
cnf(s229,plain,
( ~ spl22_63
| ~ spl22_66
| ~ spl22_74
| ~ spl22_77
| ~ spl22_84
| ~ spl22_87
| ~ spl22_132
| ~ spl22_162
| ~ spl22_172
| ~ spl22_175
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_232
| ~ spl22_240 ),
inference(sat_conversion,[],[f1451]) ).
cnf(s231,plain,
( ~ spl22_62
| ~ spl22_66
| ~ spl22_73
| ~ spl22_77
| ~ spl22_83
| ~ spl22_87
| ~ spl22_110
| ~ spl22_150
| ~ spl22_160
| ~ spl22_164
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_233
| ~ spl22_240 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s233,plain,
( ~ spl22_61
| ~ spl22_66
| ~ spl22_72
| ~ spl22_77
| ~ spl22_82
| ~ spl22_87
| ~ spl22_88
| ~ spl22_138
| ~ spl22_148
| ~ spl22_153
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_234
| ~ spl22_240 ),
inference(sat_conversion,[],[f1455]) ).
cnf(s235,plain,
( ~ spl22_201
| ~ spl22_202
| ~ spl22_203
| ~ spl22_204
| ~ spl22_205
| ~ spl22_206
| ~ spl22_207
| ~ spl22_208
| ~ spl22_209
| ~ spl22_210
| ~ spl22_211
| ~ spl22_212
| ~ spl22_213
| ~ spl22_214
| ~ spl22_215
| ~ spl22_216
| ~ spl22_219
| spl22_227 ),
inference(sat_conversion,[],[f1457]) ).
cnf(s236,plain,
( ~ spl22_61
| ~ spl22_65
| ~ spl22_72
| ~ spl22_76
| ~ spl22_86
| ~ spl22_126
| ~ spl22_148
| ~ spl22_152
| ~ spl22_192
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_234
| ~ spl22_241 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s238,plain,
( ~ spl22_61
| ~ spl22_64
| ~ spl22_72
| ~ spl22_75
| ~ spl22_84
| ~ spl22_114
| ~ spl22_148
| ~ spl22_151
| ~ spl22_181
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_234
| ~ spl22_242 ),
inference(sat_conversion,[],[f1460]) ).
cnf(s241,plain,
( ~ spl22_61
| ~ spl22_63
| ~ spl22_72
| ~ spl22_74
| ~ spl22_82
| ~ spl22_102
| ~ spl22_148
| ~ spl22_150
| ~ spl22_170
| ~ spl22_172
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_234
| ~ spl22_243 ),
inference(sat_conversion,[],[f1463]) ).
cnf(s244,plain,
( ~ spl22_61
| ~ spl22_62
| ~ spl22_72
| ~ spl22_73
| ~ spl22_80
| ~ spl22_90
| ~ spl22_148
| ~ spl22_149
| ~ spl22_159
| ~ spl22_160
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_234
| ~ spl22_244 ),
inference(sat_conversion,[],[f1466]) ).
cnf(s247,plain,
( ~ spl22_61
| ~ spl22_72
| ~ spl22_148
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_234
| ~ spl22_245 ),
inference(sat_conversion,[],[f1469]) ).
cnf(s250,plain,
( ~ spl22_60
| ~ spl22_61
| ~ spl22_71
| ~ spl22_72
| ~ spl22_87
| ~ spl22_136
| ~ spl22_137
| ~ spl22_147
| ~ spl22_148
| ~ spl22_198
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_234
| ~ spl22_246 ),
inference(sat_conversion,[],[f1472]) ).
cnf(s253,plain,
( ~ spl22_59
| ~ spl22_61
| ~ spl22_70
| ~ spl22_72
| ~ spl22_85
| ~ spl22_124
| ~ spl22_126
| ~ spl22_146
| ~ spl22_148
| ~ spl22_186
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_234
| ~ spl22_247 ),
inference(sat_conversion,[],[f1475]) ).
cnf(s256,plain,
( ~ spl22_58
| ~ spl22_61
| ~ spl22_69
| ~ spl22_72
| ~ spl22_83
| ~ spl22_112
| ~ spl22_115
| ~ spl22_145
| ~ spl22_148
| ~ spl22_174
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_234
| ~ spl22_248 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s259,plain,
( ~ spl22_57
| ~ spl22_61
| ~ spl22_68
| ~ spl22_72
| ~ spl22_81
| ~ spl22_100
| ~ spl22_104
| ~ spl22_144
| ~ spl22_148
| ~ spl22_162
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_234
| ~ spl22_249 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s262,plain,
( ~ spl22_56
| ~ spl22_61
| ~ spl22_67
| ~ spl22_72
| ~ spl22_79
| ~ spl22_93
| ~ spl22_99
| ~ spl22_148
| ~ spl22_150
| ~ spl22_154
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_234
| ~ spl22_250 ),
inference(sat_conversion,[],[f1484]) ).
cnf(s265,plain,
( ~ spl22_211
| ~ spl22_212
| ~ spl22_213
| ~ spl22_214
| ~ spl22_215
| ~ spl22_216
| ~ spl22_219
| spl22_222 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s266,plain,
( ~ spl22_213
| ~ spl22_214
| ~ spl22_215
| ~ spl22_216
| ~ spl22_219
| spl22_221 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s267,plain,
( ~ spl22_203
| ~ spl22_204
| ~ spl22_205
| ~ spl22_206
| ~ spl22_207
| ~ spl22_208
| ~ spl22_209
| ~ spl22_210
| ~ spl22_211
| ~ spl22_212
| ~ spl22_213
| ~ spl22_214
| ~ spl22_215
| ~ spl22_216
| ~ spl22_219
| spl22_226 ),
inference(sat_conversion,[],[f1489]) ).
cnf(s268,plain,
( ~ spl22_209
| ~ spl22_210
| ~ spl22_211
| ~ spl22_212
| ~ spl22_213
| ~ spl22_214
| ~ spl22_215
| ~ spl22_216
| ~ spl22_219
| spl22_223 ),
inference(sat_conversion,[],[f1490]) ).
cnf(s269,plain,
( ~ spl22_205
| ~ spl22_206
| ~ spl22_207
| ~ spl22_208
| ~ spl22_209
| ~ spl22_210
| ~ spl22_211
| ~ spl22_212
| ~ spl22_213
| ~ spl22_214
| ~ spl22_215
| ~ spl22_216
| ~ spl22_219
| spl22_225 ),
inference(sat_conversion,[],[f1491]) ).
cnf(s270,plain,
( ~ spl22_207
| ~ spl22_208
| ~ spl22_209
| ~ spl22_210
| ~ spl22_211
| ~ spl22_212
| ~ spl22_213
| ~ spl22_214
| ~ spl22_215
| ~ spl22_216
| ~ spl22_219
| spl22_224 ),
inference(sat_conversion,[],[f1492]) ).
cnf(s271,plain,
( ~ spl22_58
| ~ spl22_65
| ~ spl22_69
| ~ spl22_76
| ~ spl22_90
| ~ spl22_112
| ~ spl22_119
| ~ spl22_171
| ~ spl22_189
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_230
| ~ spl22_248 ),
inference(sat_conversion,[],[f1493]) ).
cnf(s272,plain,
( ~ spl22_58
| ~ spl22_66
| ~ spl22_69
| ~ spl22_77
| ~ spl22_79
| ~ spl22_87
| ~ spl22_102
| ~ spl22_112
| ~ spl22_120
| ~ spl22_193
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_229
| ~ spl22_248 ),
inference(sat_conversion,[],[f1494]) ).
cnf(s273,plain,
( ~ spl22_58
| ~ spl22_59
| ~ spl22_69
| ~ spl22_70
| ~ spl22_112
| ~ spl22_113
| ~ spl22_123
| ~ spl22_124
| ~ spl22_150
| ~ spl22_160
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_236
| ~ spl22_248 ),
inference(sat_conversion,[],[f1495]) ).
cnf(s274,plain,
( ~ spl22_58
| ~ spl22_60
| ~ spl22_69
| ~ spl22_71
| ~ spl22_112
| ~ spl22_114
| ~ spl22_134
| ~ spl22_136
| ~ spl22_162
| ~ spl22_182
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_235
| ~ spl22_248 ),
inference(sat_conversion,[],[f1496]) ).
cnf(s275,plain,
( ~ spl22_58
| ~ spl22_63
| ~ spl22_69
| ~ spl22_74
| ~ spl22_112
| ~ spl22_117
| ~ spl22_127
| ~ spl22_167
| ~ spl22_172
| ~ spl22_198
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_232
| ~ spl22_248 ),
inference(sat_conversion,[],[f1497]) ).
cnf(s276,plain,
( ~ spl22_56
| ~ spl22_58
| ~ spl22_67
| ~ spl22_69
| ~ spl22_90
| ~ spl22_94
| ~ spl22_99
| ~ spl22_112
| ~ spl22_114
| ~ spl22_121
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_239
| ~ spl22_248 ),
inference(sat_conversion,[],[f1498]) ).
cnf(s277,plain,
( ~ spl22_58
| ~ spl22_69
| ~ spl22_112
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_237
| ~ spl22_248 ),
inference(sat_conversion,[],[f1499]) ).
cnf(s278,plain,
( ~ spl22_57
| ~ spl22_58
| ~ spl22_68
| ~ spl22_69
| ~ spl22_100
| ~ spl22_101
| ~ spl22_111
| ~ spl22_112
| ~ spl22_116
| ~ spl22_126
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_238
| ~ spl22_248 ),
inference(sat_conversion,[],[f1500]) ).
cnf(s279,plain,
( ~ spl22_58
| ~ spl22_62
| ~ spl22_69
| ~ spl22_73
| ~ spl22_105
| ~ spl22_112
| ~ spl22_116
| ~ spl22_156
| ~ spl22_160
| ~ spl22_186
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_233
| ~ spl22_248 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s280,plain,
( ~ spl22_58
| ~ spl22_64
| ~ spl22_69
| ~ spl22_75
| ~ spl22_78
| ~ spl22_112
| ~ spl22_118
| ~ spl22_149
| ~ spl22_178
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_231
| ~ spl22_248 ),
inference(sat_conversion,[],[f1502]) ).
cnf(s281,plain,
( ~ spl22_56
| ~ spl22_64
| ~ spl22_67
| ~ spl22_75
| ~ spl22_96
| ~ spl22_99
| ~ spl22_145
| ~ spl22_184
| ~ spl22_186
| ~ spl22_187
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_231
| ~ spl22_250 ),
inference(sat_conversion,[],[f1503]) ).
cnf(s282,plain,
( ~ spl22_56
| ~ spl22_57
| ~ spl22_67
| ~ spl22_68
| ~ spl22_89
| ~ spl22_99
| ~ spl22_100
| ~ spl22_102
| ~ spl22_110
| ~ spl22_112
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_238
| ~ spl22_250 ),
inference(sat_conversion,[],[f1504]) ).
cnf(s283,plain,
( ~ spl22_56
| ~ spl22_66
| ~ spl22_67
| ~ spl22_77
| ~ spl22_78
| ~ spl22_87
| ~ spl22_88
| ~ spl22_98
| ~ spl22_99
| ~ spl22_189
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_229
| ~ spl22_250 ),
inference(sat_conversion,[],[f1505]) ).
cnf(s284,plain,
( ~ spl22_56
| ~ spl22_60
| ~ spl22_67
| ~ spl22_71
| ~ spl22_92
| ~ spl22_99
| ~ spl22_136
| ~ spl22_138
| ~ spl22_143
| ~ spl22_178
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_235
| ~ spl22_250 ),
inference(sat_conversion,[],[f1506]) ).
cnf(s285,plain,
( ~ spl22_56
| ~ spl22_59
| ~ spl22_67
| ~ spl22_70
| ~ spl22_91
| ~ spl22_99
| ~ spl22_124
| ~ spl22_126
| ~ spl22_132
| ~ spl22_156
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_236
| ~ spl22_250 ),
inference(sat_conversion,[],[f1507]) ).
cnf(s286,plain,
( ~ spl22_56
| ~ spl22_58
| ~ spl22_67
| ~ spl22_69
| ~ spl22_90
| ~ spl22_99
| ~ spl22_112
| ~ spl22_114
| ~ spl22_121
| ~ spl22_134
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_237
| ~ spl22_250 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s287,plain,
( ~ spl22_56
| ~ spl22_67
| ~ spl22_99
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_239
| ~ spl22_250 ),
inference(sat_conversion,[],[f1509]) ).
cnf(s288,plain,
( ~ spl22_56
| ~ spl22_62
| ~ spl22_67
| ~ spl22_73
| ~ spl22_94
| ~ spl22_99
| ~ spl22_101
| ~ spl22_160
| ~ spl22_162
| ~ spl22_165
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_233
| ~ spl22_250 ),
inference(sat_conversion,[],[f1510]) ).
cnf(s289,plain,
( ~ spl22_56
| ~ spl22_63
| ~ spl22_67
| ~ spl22_74
| ~ spl22_95
| ~ spl22_99
| ~ spl22_123
| ~ spl22_172
| ~ spl22_174
| ~ spl22_176
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_232
| ~ spl22_250 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s290,plain,
( ~ spl22_56
| ~ spl22_65
| ~ spl22_67
| ~ spl22_76
| ~ spl22_97
| ~ spl22_99
| ~ spl22_167
| ~ spl22_196
| ~ spl22_198
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_230
| ~ spl22_250 ),
inference(sat_conversion,[],[f1512]) ).
cnf(s291,plain,
( ~ spl22_60
| ~ spl22_64
| ~ spl22_71
| ~ spl22_75
| ~ spl22_102
| ~ spl22_136
| ~ spl22_140
| ~ spl22_153
| ~ spl22_180
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_231
| ~ spl22_246 ),
inference(sat_conversion,[],[f1513]) ).
cnf(s292,plain,
( ~ spl22_62
| ~ spl22_64
| ~ spl22_73
| ~ spl22_75
| ~ spl22_126
| ~ spl22_146
| ~ spl22_160
| ~ spl22_162
| ~ spl22_182
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_231
| ~ spl22_244 ),
inference(sat_conversion,[],[f1514]) ).
cnf(s293,plain,
( ~ spl22_59
| ~ spl22_64
| ~ spl22_70
| ~ spl22_75
| ~ spl22_90
| ~ spl22_124
| ~ spl22_129
| ~ spl22_151
| ~ spl22_179
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_231
| ~ spl22_247 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s294,plain,
( ~ spl22_63
| ~ spl22_64
| ~ spl22_74
| ~ spl22_75
| ~ spl22_138
| ~ spl22_148
| ~ spl22_172
| ~ spl22_173
| ~ spl22_183
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_231
| ~ spl22_243 ),
inference(sat_conversion,[],[f1516]) ).
cnf(s295,plain,
( ~ spl22_57
| ~ spl22_64
| ~ spl22_68
| ~ spl22_75
| ~ spl22_100
| ~ spl22_107
| ~ spl22_147
| ~ spl22_177
| ~ spl22_184
| ~ spl22_198
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_231
| ~ spl22_249 ),
inference(sat_conversion,[],[f1517]) ).
cnf(s296,plain,
( ~ spl22_64
| ~ spl22_65
| ~ spl22_75
| ~ spl22_76
| ~ spl22_152
| ~ spl22_162
| ~ spl22_184
| ~ spl22_185
| ~ spl22_195
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_231
| ~ spl22_241 ),
inference(sat_conversion,[],[f1518]) ).
cnf(s297,plain,
( ~ spl22_61
| ~ spl22_64
| ~ spl22_72
| ~ spl22_75
| ~ spl22_114
| ~ spl22_144
| ~ spl22_148
| ~ spl22_151
| ~ spl22_181
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_231
| ~ spl22_245 ),
inference(sat_conversion,[],[f1519]) ).
cnf(s298,plain,
( ~ spl22_64
| ~ spl22_75
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_231
| ~ spl22_242 ),
inference(sat_conversion,[],[f1520]) ).
cnf(s299,plain,
( ~ spl22_63
| ~ spl22_65
| ~ spl22_74
| ~ spl22_76
| ~ spl22_130
| ~ spl22_150
| ~ spl22_172
| ~ spl22_174
| ~ spl22_194
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_232
| ~ spl22_241 ),
inference(sat_conversion,[],[f1521]) ).
cnf(s300,plain,
( ~ spl22_59
| ~ spl22_65
| ~ spl22_70
| ~ spl22_76
| ~ spl22_102
| ~ spl22_124
| ~ spl22_130
| ~ spl22_163
| ~ spl22_190
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_236
| ~ spl22_241 ),
inference(sat_conversion,[],[f1522]) ).
cnf(s301,plain,
( ~ spl22_65
| ~ spl22_76
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_230
| ~ spl22_241 ),
inference(sat_conversion,[],[f1523]) ).
cnf(s302,plain,
( ~ spl22_62
| ~ spl22_65
| ~ spl22_73
| ~ spl22_76
| ~ spl22_108
| ~ spl22_138
| ~ spl22_160
| ~ spl22_163
| ~ spl22_193
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_233
| ~ spl22_241 ),
inference(sat_conversion,[],[f1524]) ).
cnf(s303,plain,
( ~ spl22_60
| ~ spl22_65
| ~ spl22_71
| ~ spl22_76
| ~ spl22_114
| ~ spl22_136
| ~ spl22_141
| ~ spl22_185
| ~ spl22_191
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_235
| ~ spl22_241 ),
inference(sat_conversion,[],[f1525]) ).
cnf(s304,plain,
( ~ spl22_65
| ~ spl22_66
| ~ spl22_76
| ~ spl22_77
| ~ spl22_86
| ~ spl22_87
| ~ spl22_186
| ~ spl22_196
| ~ spl22_197
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_229
| ~ spl22_241 ),
inference(sat_conversion,[],[f1526]) ).
cnf(s305,plain,
( ~ spl22_57
| ~ spl22_65
| ~ spl22_68
| ~ spl22_76
| ~ spl22_78
| ~ spl22_100
| ~ spl22_108
| ~ spl22_119
| ~ spl22_188
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_238
| ~ spl22_241 ),
inference(sat_conversion,[],[f1527]) ).
cnf(s306,plain,
( ~ spl22_56
| ~ spl22_65
| ~ spl22_67
| ~ spl22_76
| ~ spl22_97
| ~ spl22_99
| ~ spl22_196
| ~ spl22_198
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_239
| ~ spl22_241 ),
inference(sat_conversion,[],[f1528]) ).
cnf(s307,plain,
( ~ spl22_58
| ~ spl22_65
| ~ spl22_69
| ~ spl22_76
| ~ spl22_90
| ~ spl22_112
| ~ spl22_119
| ~ spl22_141
| ~ spl22_189
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_237
| ~ spl22_241 ),
inference(sat_conversion,[],[f1529]) ).
cnf(s308,plain,
( ~ spl22_57
| ~ spl22_59
| ~ spl22_68
| ~ spl22_70
| ~ spl22_100
| ~ spl22_102
| ~ spl22_118
| ~ spl22_122
| ~ spl22_124
| ~ spl22_138
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_238
| ~ spl22_247 ),
inference(sat_conversion,[],[f1530]) ).
cnf(s309,plain,
( ~ spl22_57
| ~ spl22_62
| ~ spl22_68
| ~ spl22_73
| ~ spl22_100
| ~ spl22_105
| ~ spl22_113
| ~ spl22_155
| ~ spl22_160
| ~ spl22_174
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_238
| ~ spl22_244 ),
inference(sat_conversion,[],[f1531]) ).
cnf(s310,plain,
( ~ spl22_57
| ~ spl22_60
| ~ spl22_68
| ~ spl22_71
| ~ spl22_100
| ~ spl22_103
| ~ spl22_120
| ~ spl22_133
| ~ spl22_136
| ~ spl22_150
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_238
| ~ spl22_246 ),
inference(sat_conversion,[],[f1532]) ).
cnf(s311,plain,
( ~ spl22_57
| ~ spl22_61
| ~ spl22_68
| ~ spl22_72
| ~ spl22_100
| ~ spl22_104
| ~ spl22_111
| ~ spl22_144
| ~ spl22_148
| ~ spl22_162
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_238
| ~ spl22_245 ),
inference(sat_conversion,[],[f1533]) ).
cnf(s312,plain,
( ~ spl22_57
| ~ spl22_68
| ~ spl22_100
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_238
| ~ spl22_249 ),
inference(sat_conversion,[],[f1534]) ).
cnf(s313,plain,
( ~ spl22_57
| ~ spl22_63
| ~ spl22_68
| ~ spl22_74
| ~ spl22_100
| ~ spl22_106
| ~ spl22_115
| ~ spl22_166
| ~ spl22_172
| ~ spl22_186
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_238
| ~ spl22_243 ),
inference(sat_conversion,[],[f1535]) ).
cnf(s314,plain,
( ~ spl22_57
| ~ spl22_66
| ~ spl22_68
| ~ spl22_77
| ~ spl22_78
| ~ spl22_87
| ~ spl22_90
| ~ spl22_100
| ~ spl22_109
| ~ spl22_121
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_238
| ~ spl22_240 ),
inference(sat_conversion,[],[f1536]) ).
cnf(s315,plain,
( ~ spl22_57
| ~ spl22_64
| ~ spl22_68
| ~ spl22_75
| ~ spl22_100
| ~ spl22_107
| ~ spl22_117
| ~ spl22_177
| ~ spl22_184
| ~ spl22_198
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_238
| ~ spl22_242 ),
inference(sat_conversion,[],[f1537]) ).
cnf(s316,plain,
( ~ spl22_58
| ~ spl22_61
| ~ spl22_69
| ~ spl22_72
| ~ spl22_112
| ~ spl22_115
| ~ spl22_133
| ~ spl22_145
| ~ spl22_148
| ~ spl22_174
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_237
| ~ spl22_245 ),
inference(sat_conversion,[],[f1538]) ).
cnf(s317,plain,
( ~ spl22_61
| ~ spl22_66
| ~ spl22_72
| ~ spl22_77
| ~ spl22_82
| ~ spl22_87
| ~ spl22_138
| ~ spl22_148
| ~ spl22_153
| ~ spl22_188
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_229
| ~ spl22_245 ),
inference(sat_conversion,[],[f1539]) ).
cnf(s318,plain,
( ~ spl22_61
| ~ spl22_62
| ~ spl22_72
| ~ spl22_73
| ~ spl22_90
| ~ spl22_100
| ~ spl22_148
| ~ spl22_149
| ~ spl22_159
| ~ spl22_160
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_233
| ~ spl22_245 ),
inference(sat_conversion,[],[f1540]) ).
cnf(s319,plain,
( ~ spl22_61
| ~ spl22_65
| ~ spl22_72
| ~ spl22_76
| ~ spl22_126
| ~ spl22_148
| ~ spl22_152
| ~ spl22_166
| ~ spl22_192
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_230
| ~ spl22_245 ),
inference(sat_conversion,[],[f1541]) ).
cnf(s320,plain,
( ~ spl22_56
| ~ spl22_61
| ~ spl22_67
| ~ spl22_72
| ~ spl22_89
| ~ spl22_93
| ~ spl22_99
| ~ spl22_148
| ~ spl22_150
| ~ spl22_154
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_239
| ~ spl22_245 ),
inference(sat_conversion,[],[f1542]) ).
cnf(s321,plain,
( ~ spl22_61
| ~ spl22_63
| ~ spl22_72
| ~ spl22_74
| ~ spl22_102
| ~ spl22_122
| ~ spl22_148
| ~ spl22_150
| ~ spl22_170
| ~ spl22_172
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_232
| ~ spl22_245 ),
inference(sat_conversion,[],[f1543]) ).
cnf(s322,plain,
( ~ spl22_59
| ~ spl22_61
| ~ spl22_70
| ~ spl22_72
| ~ spl22_124
| ~ spl22_126
| ~ spl22_146
| ~ spl22_148
| ~ spl22_155
| ~ spl22_186
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_236
| ~ spl22_245 ),
inference(sat_conversion,[],[f1544]) ).
cnf(s323,plain,
( ~ spl22_60
| ~ spl22_61
| ~ spl22_71
| ~ spl22_72
| ~ spl22_136
| ~ spl22_137
| ~ spl22_147
| ~ spl22_148
| ~ spl22_177
| ~ spl22_198
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_235
| ~ spl22_245 ),
inference(sat_conversion,[],[f1545]) ).
cnf(s324,plain,
( ~ spl22_62
| ~ spl22_66
| ~ spl22_73
| ~ spl22_77
| ~ spl22_83
| ~ spl22_87
| ~ spl22_150
| ~ spl22_160
| ~ spl22_164
| ~ spl22_190
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_229
| ~ spl22_244 ),
inference(sat_conversion,[],[f1546]) ).
cnf(s325,plain,
( ~ spl22_60
| ~ spl22_66
| ~ spl22_71
| ~ spl22_77
| ~ spl22_81
| ~ spl22_87
| ~ spl22_126
| ~ spl22_136
| ~ spl22_142
| ~ spl22_197
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_229
| ~ spl22_246 ),
inference(sat_conversion,[],[f1547]) ).
cnf(s326,plain,
( ~ spl22_57
| ~ spl22_66
| ~ spl22_68
| ~ spl22_77
| ~ spl22_78
| ~ spl22_87
| ~ spl22_90
| ~ spl22_100
| ~ spl22_109
| ~ spl22_191
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_229
| ~ spl22_249 ),
inference(sat_conversion,[],[f1548]) ).
cnf(s327,plain,
( ~ spl22_63
| ~ spl22_66
| ~ spl22_74
| ~ spl22_77
| ~ spl22_84
| ~ spl22_87
| ~ spl22_162
| ~ spl22_172
| ~ spl22_175
| ~ spl22_192
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_229
| ~ spl22_243 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s328,plain,
( ~ spl22_64
| ~ spl22_66
| ~ spl22_75
| ~ spl22_77
| ~ spl22_85
| ~ spl22_87
| ~ spl22_174
| ~ spl22_184
| ~ spl22_186
| ~ spl22_194
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_229
| ~ spl22_242 ),
inference(sat_conversion,[],[f1550]) ).
cnf(s329,plain,
( ~ spl22_59
| ~ spl22_66
| ~ spl22_70
| ~ spl22_77
| ~ spl22_80
| ~ spl22_87
| ~ spl22_114
| ~ spl22_124
| ~ spl22_131
| ~ spl22_195
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_229
| ~ spl22_247 ),
inference(sat_conversion,[],[f1551]) ).
cnf(s330,plain,
( ~ spl22_56
| ~ spl22_63
| ~ spl22_67
| ~ spl22_74
| ~ spl22_93
| ~ spl22_95
| ~ spl22_99
| ~ spl22_172
| ~ spl22_174
| ~ spl22_176
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_239
| ~ spl22_243 ),
inference(sat_conversion,[],[f1552]) ).
cnf(s331,plain,
( ~ spl22_63
| ~ spl22_65
| ~ spl22_74
| ~ spl22_76
| ~ spl22_150
| ~ spl22_170
| ~ spl22_172
| ~ spl22_174
| ~ spl22_194
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_230
| ~ spl22_243 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s332,plain,
( ~ spl22_60
| ~ spl22_63
| ~ spl22_71
| ~ spl22_74
| ~ spl22_90
| ~ spl22_136
| ~ spl22_139
| ~ spl22_169
| ~ spl22_172
| ~ spl22_181
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_235
| ~ spl22_243 ),
inference(sat_conversion,[],[f1554]) ).
cnf(s333,plain,
( ~ spl22_59
| ~ spl22_63
| ~ spl22_70
| ~ spl22_74
| ~ spl22_78
| ~ spl22_124
| ~ spl22_128
| ~ spl22_159
| ~ spl22_168
| ~ spl22_172
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_236
| ~ spl22_243 ),
inference(sat_conversion,[],[f1555]) ).
cnf(s334,plain,
( ~ spl22_62
| ~ spl22_63
| ~ spl22_73
| ~ spl22_74
| ~ spl22_104
| ~ spl22_114
| ~ spl22_160
| ~ spl22_161
| ~ spl22_171
| ~ spl22_172
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_233
| ~ spl22_243 ),
inference(sat_conversion,[],[f1556]) ).
cnf(s335,plain,
( ~ spl22_58
| ~ spl22_63
| ~ spl22_69
| ~ spl22_74
| ~ spl22_112
| ~ spl22_117
| ~ spl22_137
| ~ spl22_167
| ~ spl22_172
| ~ spl22_198
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_237
| ~ spl22_243 ),
inference(sat_conversion,[],[f1557]) ).
cnf(s336,plain,
( ~ spl22_63
| ~ spl22_74
| ~ spl22_172
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_232
| ~ spl22_243 ),
inference(sat_conversion,[],[f1558]) ).
cnf(s337,plain,
( ~ spl22_59
| ~ spl22_70
| ~ spl22_124
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_236
| ~ spl22_247 ),
inference(sat_conversion,[],[f1559]) ).
cnf(s338,plain,
( ~ spl22_59
| ~ spl22_64
| ~ spl22_70
| ~ spl22_75
| ~ spl22_90
| ~ spl22_124
| ~ spl22_129
| ~ spl22_161
| ~ spl22_179
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_236
| ~ spl22_242 ),
inference(sat_conversion,[],[f1560]) ).
cnf(s339,plain,
( ~ spl22_59
| ~ spl22_66
| ~ spl22_70
| ~ spl22_77
| ~ spl22_80
| ~ spl22_87
| ~ spl22_114
| ~ spl22_124
| ~ spl22_131
| ~ spl22_165
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_236
| ~ spl22_240 ),
inference(sat_conversion,[],[f1561]) ).
cnf(s340,plain,
( ~ spl22_59
| ~ spl22_62
| ~ spl22_70
| ~ spl22_73
| ~ spl22_124
| ~ spl22_127
| ~ spl22_157
| ~ spl22_160
| ~ spl22_198
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_236
| ~ spl22_244 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s341,plain,
( ~ spl22_59
| ~ spl22_60
| ~ spl22_70
| ~ spl22_71
| ~ spl22_124
| ~ spl22_125
| ~ spl22_135
| ~ spl22_136
| ~ spl22_164
| ~ spl22_174
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_236
| ~ spl22_246 ),
inference(sat_conversion,[],[f1563]) ).
cnf(s342,plain,
( ~ spl22_57
| ~ spl22_59
| ~ spl22_68
| ~ spl22_70
| ~ spl22_100
| ~ spl22_102
| ~ spl22_122
| ~ spl22_124
| ~ spl22_138
| ~ spl22_158
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_236
| ~ spl22_249 ),
inference(sat_conversion,[],[f1564]) ).
cnf(s343,plain,
( ~ spl22_60
| ~ spl22_62
| ~ spl22_71
| ~ spl22_73
| ~ spl22_78
| ~ spl22_136
| ~ spl22_138
| ~ spl22_158
| ~ spl22_160
| ~ spl22_179
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_235
| ~ spl22_244 ),
inference(sat_conversion,[],[f1565]) ).
cnf(s344,plain,
( ~ spl22_58
| ~ spl22_62
| ~ spl22_69
| ~ spl22_73
| ~ spl22_112
| ~ spl22_116
| ~ spl22_135
| ~ spl22_156
| ~ spl22_160
| ~ spl22_186
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_237
| ~ spl22_244 ),
inference(sat_conversion,[],[f1566]) ).
cnf(s345,plain,
( ~ spl22_62
| ~ spl22_65
| ~ spl22_73
| ~ spl22_76
| ~ spl22_138
| ~ spl22_160
| ~ spl22_163
| ~ spl22_168
| ~ spl22_193
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_230
| ~ spl22_244 ),
inference(sat_conversion,[],[f1567]) ).
cnf(s346,plain,
( ~ spl22_62
| ~ spl22_63
| ~ spl22_73
| ~ spl22_74
| ~ spl22_114
| ~ spl22_124
| ~ spl22_160
| ~ spl22_161
| ~ spl22_171
| ~ spl22_172
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_232
| ~ spl22_244 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s347,plain,
( ~ spl22_62
| ~ spl22_73
| ~ spl22_160
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_233
| ~ spl22_244 ),
inference(sat_conversion,[],[f1569]) ).
cnf(s348,plain,
( ~ spl22_56
| ~ spl22_62
| ~ spl22_67
| ~ spl22_73
| ~ spl22_91
| ~ spl22_94
| ~ spl22_99
| ~ spl22_160
| ~ spl22_162
| ~ spl22_165
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_239
| ~ spl22_244 ),
inference(sat_conversion,[],[f1570]) ).
cnf(s349,plain,
( ~ spl22_59
| ~ spl22_65
| ~ spl22_70
| ~ spl22_76
| ~ spl22_102
| ~ spl22_124
| ~ spl22_130
| ~ spl22_173
| ~ spl22_190
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_230
| ~ spl22_247 ),
inference(sat_conversion,[],[f1571]) ).
cnf(s350,plain,
( ~ spl22_60
| ~ spl22_65
| ~ spl22_71
| ~ spl22_76
| ~ spl22_114
| ~ spl22_136
| ~ spl22_141
| ~ spl22_175
| ~ spl22_191
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_230
| ~ spl22_246 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s351,plain,
( ~ spl22_57
| ~ spl22_65
| ~ spl22_68
| ~ spl22_76
| ~ spl22_78
| ~ spl22_100
| ~ spl22_108
| ~ spl22_169
| ~ spl22_188
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_230
| ~ spl22_249 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s352,plain,
( ~ spl22_64
| ~ spl22_65
| ~ spl22_75
| ~ spl22_76
| ~ spl22_162
| ~ spl22_172
| ~ spl22_184
| ~ spl22_185
| ~ spl22_195
| ~ spl22_196
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_230
| ~ spl22_242 ),
inference(sat_conversion,[],[f1574]) ).
cnf(s353,plain,
( ~ spl22_59
| ~ spl22_60
| ~ spl22_70
| ~ spl22_71
| ~ spl22_124
| ~ spl22_125
| ~ spl22_135
| ~ spl22_136
| ~ spl22_174
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_235
| ~ spl22_247 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s354,plain,
( ~ spl22_59
| ~ spl22_62
| ~ spl22_70
| ~ spl22_73
| ~ spl22_107
| ~ spl22_124
| ~ spl22_127
| ~ spl22_157
| ~ spl22_160
| ~ spl22_198
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_233
| ~ spl22_247 ),
inference(sat_conversion,[],[f1576]) ).
cnf(s355,plain,
( ~ spl22_59
| ~ spl22_63
| ~ spl22_70
| ~ spl22_74
| ~ spl22_78
| ~ spl22_124
| ~ spl22_128
| ~ spl22_129
| ~ spl22_168
| ~ spl22_172
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_232
| ~ spl22_247 ),
inference(sat_conversion,[],[f1577]) ).
cnf(s356,plain,
( ~ spl22_58
| ~ spl22_59
| ~ spl22_69
| ~ spl22_70
| ~ spl22_112
| ~ spl22_113
| ~ spl22_123
| ~ spl22_124
| ~ spl22_140
| ~ spl22_150
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_237
| ~ spl22_247 ),
inference(sat_conversion,[],[f1578]) ).
cnf(s357,plain,
( ~ spl22_56
| ~ spl22_59
| ~ spl22_67
| ~ spl22_70
| ~ spl22_91
| ~ spl22_96
| ~ spl22_99
| ~ spl22_124
| ~ spl22_126
| ~ spl22_132
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_239
| ~ spl22_247 ),
inference(sat_conversion,[],[f1579]) ).
cnf(s358,plain,
( ~ spl22_57
| ~ spl22_63
| ~ spl22_68
| ~ spl22_74
| ~ spl22_100
| ~ spl22_106
| ~ spl22_125
| ~ spl22_166
| ~ spl22_172
| ~ spl22_186
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_232
| ~ spl22_249 ),
inference(sat_conversion,[],[f1580]) ).
cnf(s359,plain,
( ~ spl22_60
| ~ spl22_63
| ~ spl22_71
| ~ spl22_74
| ~ spl22_90
| ~ spl22_131
| ~ spl22_136
| ~ spl22_139
| ~ spl22_169
| ~ spl22_172
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_232
| ~ spl22_246 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s360,plain,
( ~ spl22_63
| ~ spl22_64
| ~ spl22_74
| ~ spl22_75
| ~ spl22_128
| ~ spl22_138
| ~ spl22_172
| ~ spl22_173
| ~ spl22_183
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_232
| ~ spl22_242 ),
inference(sat_conversion,[],[f1582]) ).
cnf(s361,plain,
( ~ spl22_60
| ~ spl22_64
| ~ spl22_71
| ~ spl22_75
| ~ spl22_102
| ~ spl22_136
| ~ spl22_140
| ~ spl22_180
| ~ spl22_183
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_235
| ~ spl22_242 ),
inference(sat_conversion,[],[f1583]) ).
cnf(s362,plain,
( ~ spl22_62
| ~ spl22_64
| ~ spl22_73
| ~ spl22_75
| ~ spl22_106
| ~ spl22_126
| ~ spl22_160
| ~ spl22_162
| ~ spl22_182
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_233
| ~ spl22_242 ),
inference(sat_conversion,[],[f1584]) ).
cnf(s363,plain,
( ~ spl22_56
| ~ spl22_64
| ~ spl22_67
| ~ spl22_75
| ~ spl22_95
| ~ spl22_96
| ~ spl22_99
| ~ spl22_184
| ~ spl22_186
| ~ spl22_187
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_239
| ~ spl22_242 ),
inference(sat_conversion,[],[f1585]) ).
cnf(s364,plain,
( ~ spl22_58
| ~ spl22_64
| ~ spl22_69
| ~ spl22_75
| ~ spl22_78
| ~ spl22_112
| ~ spl22_118
| ~ spl22_139
| ~ spl22_178
| ~ spl22_184
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_237
| ~ spl22_242 ),
inference(sat_conversion,[],[f1586]) ).
cnf(s365,plain,
( ~ spl22_60
| ~ spl22_62
| ~ spl22_71
| ~ spl22_73
| ~ spl22_78
| ~ spl22_109
| ~ spl22_136
| ~ spl22_138
| ~ spl22_158
| ~ spl22_160
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_233
| ~ spl22_246 ),
inference(sat_conversion,[],[f1587]) ).
cnf(s366,plain,
( ~ spl22_57
| ~ spl22_62
| ~ spl22_68
| ~ spl22_73
| ~ spl22_100
| ~ spl22_103
| ~ spl22_105
| ~ spl22_155
| ~ spl22_160
| ~ spl22_174
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_233
| ~ spl22_249 ),
inference(sat_conversion,[],[f1588]) ).
cnf(s367,plain,
( ~ spl22_60
| ~ spl22_66
| ~ spl22_71
| ~ spl22_77
| ~ spl22_81
| ~ spl22_87
| ~ spl22_126
| ~ spl22_136
| ~ spl22_142
| ~ spl22_187
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_235
| ~ spl22_240 ),
inference(sat_conversion,[],[f1589]) ).
cnf(s368,plain,
( ~ spl22_56
| ~ spl22_66
| ~ spl22_67
| ~ spl22_77
| ~ spl22_78
| ~ spl22_87
| ~ spl22_88
| ~ spl22_98
| ~ spl22_99
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_239
| ~ spl22_240 ),
inference(sat_conversion,[],[f1590]) ).
cnf(s369,plain,
( ~ spl22_58
| ~ spl22_66
| ~ spl22_69
| ~ spl22_77
| ~ spl22_79
| ~ spl22_87
| ~ spl22_102
| ~ spl22_112
| ~ spl22_120
| ~ spl22_143
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_237
| ~ spl22_240 ),
inference(sat_conversion,[],[f1591]) ).
cnf(s370,plain,
( ~ spl22_60
| ~ spl22_71
| ~ spl22_136
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_235
| ~ spl22_246 ),
inference(sat_conversion,[],[f1592]) ).
cnf(s371,plain,
( ~ spl22_57
| ~ spl22_60
| ~ spl22_68
| ~ spl22_71
| ~ spl22_100
| ~ spl22_103
| ~ spl22_133
| ~ spl22_136
| ~ spl22_150
| ~ spl22_180
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_235
| ~ spl22_249 ),
inference(sat_conversion,[],[f1593]) ).
cnf(s372,plain,
( ~ spl22_57
| ~ spl22_58
| ~ spl22_68
| ~ spl22_69
| ~ spl22_100
| ~ spl22_101
| ~ spl22_111
| ~ spl22_112
| ~ spl22_126
| ~ spl22_136
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_237
| ~ spl22_249 ),
inference(sat_conversion,[],[f1594]) ).
cnf(s373,plain,
( ~ spl22_56
| ~ spl22_57
| ~ spl22_67
| ~ spl22_68
| ~ spl22_89
| ~ spl22_92
| ~ spl22_99
| ~ spl22_100
| ~ spl22_102
| ~ spl22_110
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_239
| ~ spl22_249 ),
inference(sat_conversion,[],[f1595]) ).
cnf(s374,plain,
( ~ spl22_58
| ~ spl22_60
| ~ spl22_69
| ~ spl22_71
| ~ spl22_112
| ~ spl22_114
| ~ spl22_134
| ~ spl22_136
| ~ spl22_142
| ~ spl22_162
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_237
| ~ spl22_246 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s375,plain,
( ~ spl22_56
| ~ spl22_60
| ~ spl22_67
| ~ spl22_71
| ~ spl22_92
| ~ spl22_98
| ~ spl22_99
| ~ spl22_136
| ~ spl22_138
| ~ spl22_143
| ~ spl22_217
| ~ spl22_218
| spl22_219
| ~ spl22_239
| ~ spl22_246 ),
inference(sat_conversion,[],[f1597]) ).
cnf(s376,plain,
( ~ spl22_239
| spl22_219 ),
inference(rat,[],[s221,s276,s287,s306,s320,s330,s348,s357,s363,s368,s373,s375,s60,s143,s138,s136,s71,s57,s110,s102,s100,s92,s68,s66,s98,s88,s87,s78,s77,s64,s187,s186,s184,s75,s59,s132,s126,s124,s96,s70,s62,s165,s162,s160,s91,s73,s63,s176,s174,s172,s95,s74,s61,s154,s150,s148,s93,s89,s72,s65,s198,s196,s97,s76,s56,s58,s218,s217,s121,s114,s112,s99,s94,s90,s69,s67]) ).
cnf(s377,plain,
( ~ spl22_238
| spl22_219 ),
inference(rat,[],[s221,s282,s278,s305,s308,s309,s310,s311,s312,s313,s314,s315,s64,s198,s184,s177,s117,s107,s75,s66,s121,s109,s90,s87,s77,s63,s186,s172,s166,s115,s106,s74,s61,s162,s148,s144,s104,s72,s60,s150,s136,s133,s120,s103,s71,s62,s174,s160,s155,s113,s105,s73,s59,s138,s124,s122,s118,s70,s65,s196,s188,s119,s108,s78,s76,s58,s126,s116,s111,s101,s69,s56,s57,s218,s217,s112,s110,s102,s100,s99,s89,s68,s67]) ).
cnf(s378,plain,
( ~ spl22_237
| spl22_219 ),
inference(rat,[],[s221,s286,s372,s277,s307,s316,s335,s344,s356,s364,s369,s374,s60,s162,s142,s71,s66,s143,s120,s102,s87,s79,s77,s64,s184,s178,s139,s118,s78,s75,s59,s150,s140,s124,s123,s113,s70,s62,s186,s160,s156,s135,s116,s73,s63,s198,s172,s167,s137,s117,s74,s61,s174,s148,s145,s133,s115,s72,s65,s196,s189,s141,s119,s76,s57,s136,s126,s111,s101,s100,s68,s56,s58,s218,s217,s134,s121,s114,s112,s99,s90,s69,s67]) ).
cnf(s379,plain,
( ~ spl22_236
| spl22_219 ),
inference(rat,[],[s221,s285,s342,s273,s300,s322,s333,s337,s338,s339,s340,s341,s60,s174,s164,s136,s135,s125,s71,s62,s198,s157,s127,s73,s66,s165,s131,s114,s87,s80,s77,s64,s184,s179,s161,s129,s90,s75,s63,s172,s168,s159,s128,s78,s74,s61,s186,s155,s148,s146,s72,s65,s196,s190,s163,s130,s76,s58,s160,s150,s123,s113,s112,s69,s57,s158,s138,s122,s102,s100,s68,s56,s59,s218,s217,s156,s132,s126,s124,s99,s91,s70,s67]) ).
cnf(s380,plain,
( ~ spl22_235
| spl22_219 ),
inference(rat,[],[s221,s284,s371,s274,s353,s303,s323,s332,s343,s361,s367,s370,s66,s187,s142,s126,s87,s81,s77,s64,s183,s140,s102,s75,s62,s179,s160,s158,s78,s73,s63,s181,s172,s169,s139,s90,s74,s61,s198,s177,s148,s147,s137,s72,s65,s196,s191,s185,s141,s76,s59,s184,s174,s135,s125,s124,s70,s58,s182,s162,s134,s114,s112,s69,s57,s180,s150,s133,s103,s100,s68,s56,s60,s218,s217,s178,s143,s138,s136,s99,s92,s71,s67]) ).
cnf(s381,plain,
( ~ spl22_234
| spl22_219 ),
inference(rat,[],[s221,s236,s238,s241,s244,s247,s250,s253,s256,s259,s262,s233,s66,s153,s138,s88,s77,s56,s154,s99,s93,s79,s67,s57,s162,s144,s104,s100,s81,s68,s58,s174,s145,s115,s112,s83,s69,s59,s186,s146,s124,s85,s70,s60,s198,s147,s137,s136,s87,s71,s62,s160,s159,s149,s90,s80,s73,s63,s172,s170,s150,s102,s82,s74,s64,s184,s181,s151,s114,s84,s75,s61,s65,s218,s217,s196,s192,s152,s148,s126,s86,s76,s72]) ).
cnf(s386,plain,
( ~ spl22_229
| spl22_219 ),
inference(rat,[],[s221,s283,s326,s272,s329,s325,s317,s324,s327,s328,s304,s222,s65,s196,s86,s76,s64,s194,s186,s184,s174,s85,s75,s63,s192,s175,s172,s162,s84,s74,s62,s190,s164,s160,s150,s83,s73,s61,s188,s153,s148,s138,s82,s72,s60,s197,s142,s136,s126,s81,s71,s59,s195,s131,s124,s114,s80,s70,s58,s193,s120,s112,s102,s79,s69,s57,s191,s109,s100,s90,s68,s56,s66,s218,s217,s189,s99,s98,s88,s87,s78,s77,s67]) ).
cnf(s387,plain,
( ~ spl22_250
| spl22_219 ),
inference(rat,[],[s220,s288,s289,s281,s290,s376,s377,s378,s379,s380,s381,s386,s67,s73,s94,s99,s101,s160,s162,s165,s217,s218,s62,s56,s74,s95,s123,s172,s174,s176,s63,s75,s96,s145,s184,s186,s187,s64,s76,s97,s167,s196,s198,s65]) ).
cnf(s388,plain,
( ~ spl22_249
| spl22_219 ),
inference(rat,[],[s220,s366,s358,s295,s351,s376,s377,s378,s379,s380,s381,s386,s68,s73,s100,s103,s105,s155,s160,s174,s217,s218,s62,s57,s74,s106,s125,s166,s172,s186,s63,s75,s107,s147,s177,s184,s198,s64,s76,s78,s108,s169,s188,s196,s65]) ).
cnf(s389,plain,
( ~ spl22_248
| spl22_219 ),
inference(rat,[],[s220,s279,s275,s280,s271,s376,s377,s378,s379,s380,s381,s386,s69,s73,s105,s112,s116,s156,s160,s186,s217,s218,s62,s58,s74,s117,s127,s167,s172,s198,s63,s75,s78,s118,s149,s178,s184,s64,s76,s90,s119,s171,s189,s196,s65]) ).
cnf(s390,plain,
( ~ spl22_247
| spl22_219 ),
inference(rat,[],[s220,s354,s355,s293,s349,s376,s377,s378,s379,s380,s381,s386,s70,s73,s107,s124,s127,s157,s160,s198,s217,s218,s62,s59,s74,s78,s128,s129,s168,s172,s63,s75,s90,s151,s179,s184,s64,s76,s102,s130,s173,s190,s196,s65]) ).
cnf(s391,plain,
( ~ spl22_246
| spl22_219 ),
inference(rat,[],[s220,s365,s359,s291,s350,s376,s377,s378,s379,s380,s381,s386,s71,s73,s78,s109,s136,s138,s158,s160,s217,s218,s62,s60,s74,s90,s131,s139,s169,s172,s63,s75,s102,s140,s153,s180,s184,s64,s76,s114,s141,s175,s191,s196,s65]) ).
cnf(s392,plain,
( ~ spl22_245
| spl22_219 ),
inference(rat,[],[s220,s318,s321,s297,s319,s376,s377,s378,s379,s380,s381,s386,s72,s73,s90,s100,s148,s149,s159,s160,s217,s218,s62,s61,s74,s102,s122,s150,s170,s172,s63,s75,s114,s144,s151,s181,s184,s64,s76,s126,s152,s166,s192,s196,s65]) ).
cnf(s393,plain,
( ~ spl22_244
| spl22_219 ),
inference(rat,[],[s220,s346,s292,s345,s347,s376,s377,s378,s379,s380,s381,s386,s73,s74,s114,s124,s160,s161,s171,s172,s217,s218,s63,s62,s75,s126,s146,s162,s182,s184,s64,s76,s138,s163,s168,s193,s196,s65]) ).
cnf(s394,plain,
( ~ spl22_243
| spl22_219 ),
inference(rat,[],[s220,s334,s294,s331,s336,s376,s377,s378,s379,s380,s381,s386,s73,s74,s104,s114,s160,s161,s171,s172,s217,s218,s63,s62,s75,s138,s148,s173,s183,s184,s64,s76,s150,s170,s174,s194,s196,s65]) ).
cnf(s395,plain,
( ~ spl22_242
| spl22_219 ),
inference(rat,[],[s220,s360,s362,s352,s298,s376,s377,s378,s379,s380,s381,s386,s74,s75,s128,s138,s172,s173,s183,s184,s217,s218,s64,s63,s73,s106,s126,s160,s162,s182,s62,s76,s185,s195,s196,s65]) ).
cnf(s396,plain,
( ~ spl22_241
| spl22_219 ),
inference(rat,[],[s220,s296,s299,s302,s301,s376,s377,s378,s379,s380,s381,s386,s75,s76,s152,s162,s184,s185,s195,s196,s217,s218,s65,s64,s74,s130,s150,s172,s174,s194,s63,s73,s108,s138,s160,s163,s193,s62]) ).
cnf(s397,plain,
spl22_219,
inference(rat,[],[s220,s225,s227,s229,s231,s221,s396,s395,s394,s393,s392,s391,s390,s389,s388,s387,s386,s381,s380,s379,s378,s377,s376,s76,s77,s86,s87,s176,s186,s196,s197,s217,s218,s66,s65,s75,s85,s154,s174,s184,s64,s74,s84,s132,s162,s172,s175,s63,s73,s83,s110,s150,s160,s164,s62]) ).
cnf(s398,plain,
spl22_220,
inference(rat,[],[s224,s215,s216,s397]) ).
cnf(s399,plain,
spl22_221,
inference(rat,[],[s266,s213,s214,s216,s215,s397]) ).
cnf(s400,plain,
spl22_222,
inference(rat,[],[s265,s211,s212,s216,s215,s214,s213,s397]) ).
cnf(s401,plain,
spl22_223,
inference(rat,[],[s268,s209,s210,s216,s215,s214,s213,s212,s211,s397]) ).
cnf(s402,plain,
spl22_224,
inference(rat,[],[s270,s207,s208,s216,s215,s214,s213,s212,s211,s210,s209,s397]) ).
cnf(s403,plain,
spl22_225,
inference(rat,[],[s269,s205,s206,s216,s215,s214,s213,s212,s211,s210,s209,s208,s207,s397]) ).
cnf(s404,plain,
spl22_226,
inference(rat,[],[s267,s203,s204,s216,s215,s214,s213,s212,s211,s210,s209,s208,s207,s206,s205,s397]) ).
cnf(s405,plain,
spl22_227,
inference(rat,[],[s235,s201,s202,s216,s215,s214,s213,s212,s211,s210,s209,s208,s207,s206,s205,s204,s203,s397]) ).
cnf(s406,plain,
spl22_228,
inference(rat,[],[s223,s199,s200,s216,s215,s214,s213,s212,s211,s210,s209,s208,s207,s206,s205,s204,s203,s202,s201,s397]) ).
cnf(s407,plain,
$false,
inference(rat,[],[s219,s406,s405,s404,s403,s402,s401,s400,s397,s399,s398]) ).
fof(f1598,plain,
$false,
inference(avatar_sat_refutation,[],[s407]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM377+1.010 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n013.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 19:42:52 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.58/2.07 % (510091)Detected formulas, will run a generic FOF schedule.
% 2.58/2.07 % (510117)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=208191334:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.58/2.07 % (510117)Refutation not found, incomplete strategy
% 2.58/2.07 % (510117)------------------------------
% 2.58/2.07 % (510117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.58/2.07 % (510117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/2.07 % (510117)CaDiCaL version: 2.1.3
% 2.58/2.07 % (510117)Termination reason: Refutation not found, incomplete strategy
% 2.58/2.07 % (510117)Time elapsed: 0.0000 s
% 2.58/2.07 % (510117)Peak memory usage: 86 MB
% 2.58/2.07 % (510119)dis-21_1_sil=8000:lcm=predicate:random_seed=2426330296:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.58/2.07 % (510119)Refutation not found, incomplete strategy
% 2.58/2.07 % (510119)------------------------------
% 2.58/2.07 % (510119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.58/2.07 % (510119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/2.07 % (510119)CaDiCaL version: 2.1.3
% 2.58/2.07 % (510119)Termination reason: Refutation not found, incomplete strategy
% 2.58/2.07 % (510119)Time elapsed: 0.006 s
% 2.58/2.07 % (510119)Peak memory usage: 88 MB
% 2.58/2.07 % (510119)Instructions burned: 10 (million)
% 2.58/2.07 % (510113)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2981752042:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.58/2.07 % (510114)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3753198108:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.58/2.07 % (510115)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3207055400:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.58/2.07 % (510116)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=159199592:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.58/2.07 % (510116)Refutation not found, incomplete strategy
% 2.58/2.07 % (510116)------------------------------
% 2.58/2.07 % (510116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.58/2.07 % (510116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/2.07 % (510116)CaDiCaL version: 2.1.3
% 2.58/2.07 % (510116)Termination reason: Refutation not found, incomplete strategy
% 2.58/2.07 % (510116)Time elapsed: 0.001 s
% 2.58/2.07 % (510116)Peak memory usage: 86 MB
% 2.58/2.07 % (510118)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3875474865:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.58/2.07 % (510117)------------------------------
% 2.58/2.07 % (510117)------------------------------
% 2.58/2.07 % (510118)Instruction limit reached!
% 2.58/2.07 % (510118)------------------------------
% 2.58/2.07 % (510118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.58/2.07 % (510118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/2.07 % (510118)CaDiCaL version: 2.1.3
% 2.58/2.07 % (510118)Termination reason: Instruction limit
% 2.58/2.07 % (510118)Termination phase: Saturation
% 2.58/2.07 % (510118)Time elapsed: 0.129 s
% 2.58/2.07 % (510118)Peak memory usage: 90 MB
% 2.58/2.07 % (510118)Instructions burned: 139 (million)
% 2.58/2.07 % (510119)------------------------------
% 2.58/2.07 % (510119)------------------------------
% 2.58/2.07 % (510132)lrs+10_1_sil=8000:sp=occurrence:random_seed=200160637:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 2.58/2.07 % (510132)Refutation not found, incomplete strategy
% 2.58/2.07 % (510132)------------------------------
% 2.58/2.07 % (510132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.58/2.07 % (510132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/2.07 % (510132)CaDiCaL version: 2.1.3
% 2.58/2.07 % (510132)Termination reason: Refutation not found, incomplete strategy
% 2.58/2.07 % (510132)Time elapsed: 0.001 s
% 2.58/2.07 % (510132)Peak memory usage: 86 MB
% 2.58/2.07 [W927 19:42:53.550419520 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.42/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.42/2.40 [W927 19:42:53.550457446 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.42/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.42/2.40 [W927 19:42:53.550484376 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.42/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.42/2.40 [W927 19:42:53.550493155 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.42/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.42/2.40 [W927 19:42:53.550513556 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.42/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.42/2.40 [W927 19:42:53.550521166 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.42/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.42/2.40 % (510116)------------------------------
% 9.42/2.40 % (510116)------------------------------
% 9.42/2.40 % (510133)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3406000031:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 9.42/2.40 % (510133)Refutation not found, incomplete strategy
% 9.42/2.40 % (510133)------------------------------
% 9.42/2.40 % (510133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.42/2.40 % (510133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.42/2.40 % (510133)CaDiCaL version: 2.1.3
% 9.42/2.40 % (510133)Termination reason: Refutation not found, incomplete strategy
% 9.42/2.40 % (510133)Time elapsed: 0.002 s
% 9.42/2.40 % (510133)Peak memory usage: 87 MB
% 9.42/2.40 % (510133)Instructions burned: 1 (million)
% 9.42/2.40 % (510139)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2414288369:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 9.42/2.40 % (510139)Refutation not found, incomplete strategy
% 9.42/2.40 % (510139)------------------------------
% 9.42/2.40 % (510139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.42/2.40 % (510139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.42/2.40 % (510139)CaDiCaL version: 2.1.3
% 9.42/2.40 % (510139)Termination reason: Refutation not found, incomplete strategy
% 9.42/2.40 % (510139)Time elapsed: 0.001 s
% 9.42/2.40 % (510139)Peak memory usage: 86 MB
% 9.42/2.40 [W927 19:42:53.765277208 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.42/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.42/2.40 [W927 19:42:53.765322422 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.42/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.42/2.40 [W927 19:42:53.765384395 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.42/2.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:53.765423135 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:53.765470445 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:53.765497049 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 % (510142)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2187109155:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 17.73/3.54 [W927 19:42:53.828571695 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:53.828614848 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:53.828677392 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:53.828698658 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:53.828749658 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:53.828770105 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 % (510132)------------------------------
% 17.73/3.54 % (510132)------------------------------
% 17.73/3.54 % (510133)------------------------------
% 17.73/3.54 % (510133)------------------------------
% 17.73/3.54 % (510149)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2782169007:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 17.73/3.54 % (510149)Refutation not found, incomplete strategy
% 17.73/3.54 % (510149)------------------------------
% 17.73/3.54 % (510149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.54 % (510149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.54 % (510149)CaDiCaL version: 2.1.3
% 17.73/3.54 % (510149)Termination reason: Refutation not found, incomplete strategy
% 17.73/3.54 % (510149)Time elapsed: 0.001 s
% 17.73/3.54 % (510149)Peak memory usage: 86 MB
% 17.73/3.54 % (510142)Instruction limit reached!
% 17.73/3.54 % (510142)------------------------------
% 17.73/3.54 % (510142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.54 % (510142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.54 % (510142)CaDiCaL version: 2.1.3
% 17.73/3.54 % (510142)Termination reason: Instruction limit
% 17.73/3.54 % (510142)Termination phase: Saturation
% 17.73/3.54 % (510142)Time elapsed: 0.224 s
% 17.73/3.54 % (510142)Peak memory usage: 89 MB
% 17.73/3.54 % (510142)Instructions burned: 248 (million)
% 17.73/3.54 % (510139)------------------------------
% 17.73/3.54 % (510139)------------------------------
% 17.73/3.54 % (510150)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1126251886:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 17.73/3.54 % (510115)Refutation not found, incomplete strategy
% 17.73/3.54 % (510115)------------------------------
% 17.73/3.54 % (510115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.54 % (510115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.54 % (510115)CaDiCaL version: 2.1.3
% 17.73/3.54 % (510115)Termination reason: Refutation not found, incomplete strategy
% 17.73/3.54 % (510115)Time elapsed: 0.925 s
% 17.73/3.54 % (510115)Peak memory usage: 129 MB
% 17.73/3.54 % (510115)Instructions burned: 844 (million)
% 17.73/3.54 % (510152)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1567645924:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 17.73/3.54 % (510152)Refutation not found, incomplete strategy
% 17.73/3.54 % (510152)------------------------------
% 17.73/3.54 % (510152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.54 % (510152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.54 % (510152)CaDiCaL version: 2.1.3
% 17.73/3.54 % (510152)Termination reason: Refutation not found, incomplete strategy
% 17.73/3.54 % (510152)Time elapsed: 0.007 s
% 17.73/3.54 % (510152)Peak memory usage: 88 MB
% 17.73/3.54 % (510152)Instructions burned: 7 (million)
% 17.73/3.54 % (510154)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4184398747:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 17.73/3.54 % (510154)Refutation not found, incomplete strategy
% 17.73/3.54 % (510154)------------------------------
% 17.73/3.54 % (510154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.54 % (510154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.54 % (510154)CaDiCaL version: 2.1.3
% 17.73/3.54 % (510154)Termination reason: Refutation not found, incomplete strategy
% 17.73/3.54 % (510154)Time elapsed: 0.004 s
% 17.73/3.54 % (510154)Peak memory usage: 88 MB
% 17.73/3.54 % (510154)Instructions burned: 3 (million)
% 17.73/3.54 [W927 19:42:54.348544998 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:54.348564976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:54.348585877 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:54.348597244 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:54.348610336 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 [W927 19:42:54.348617039 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.73/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.73/3.54 % (510149)------------------------------
% 17.73/3.54 % (510149)------------------------------
% 17.73/3.54 % (510115)------------------------------
% 17.73/3.54 % (510115)------------------------------
% 17.73/3.54 % (510164)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4026067759:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 17.73/3.54 % (510152)------------------------------
% 17.73/3.54 % (510152)------------------------------
% 17.73/3.54 % (510166)lrs+10_1_sil=8000:sp=occurrence:random_seed=1263692713:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 17.73/3.54 % (510166)Refutation not found, incomplete strategy
% 17.73/3.54 % (510166)------------------------------
% 17.73/3.54 % (510166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.54 % (510166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.54 % (510166)CaDiCaL version: 2.1.3
% 17.73/3.54 % (510166)Termination reason: Refutation not found, incomplete strategy
% 17.73/3.54 % (510166)Time elapsed: 0.0000 s
% 17.73/3.54 % (510166)Peak memory usage: 86 MB
% 17.73/3.54 % (510164)Instruction limit reached!
% 17.73/3.54 % (510164)------------------------------
% 17.73/3.54 % (510164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.54 % (510164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.54 % (510164)CaDiCaL version: 2.1.3
% 17.73/3.54 % (510164)Termination reason: Instruction limit
% 17.73/3.54 % (510164)Termination phase: Saturation
% 17.73/3.54 % (510164)Time elapsed: 0.088 s
% 17.73/3.54 % (510164)Peak memory usage: 89 MB
% 17.73/3.54 % (510164)Instructions burned: 114 (million)
% 17.73/3.54 % (510154)------------------------------
% 17.73/3.54 % (510154)------------------------------
% 17.73/3.54 % (510169)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2405206139:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 17.73/3.54 % (510169)Refutation not found, incomplete strategy
% 17.73/3.54 % (510169)------------------------------
% 17.73/3.54 % (510169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.54 % (510169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.54 % (510169)CaDiCaL version: 2.1.3
% 17.73/3.54 % (510169)Termination reason: Refutation not found, incomplete strategy
% 17.73/3.54 % (510169)Time elapsed: 0.008 s
% 17.73/3.54 % (510169)Peak memory usage: 88 MB
% 17.73/3.54 % (510169)Instructions burned: 7 (million)
% 17.73/3.54 % (510166)------------------------------
% 17.73/3.54 % (510166)------------------------------
% 17.73/3.54 % (510171)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2520424787:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 17.73/3.54 % (510173)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1249782504:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 17.73/3.54 % (510173)First to succeed.
% 17.73/3.54 % (510178)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1956494490:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 17.73/3.54 % (510178)Refutation not found, incomplete strategy
% 17.73/3.54 % (510178)------------------------------
% 17.73/3.54 % (510178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.54 % (510178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.54 % (510178)CaDiCaL version: 2.1.3
% 17.73/3.54 % (510178)Termination reason: Refutation not found, incomplete strategy
% 17.73/3.54 % (510178)Time elapsed: 0.0000 s
% 17.73/3.54 % (510178)Peak memory usage: 86 MB
% 17.73/3.54 % (510173)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-510091"
% 17.73/3.54 % (510169)------------------------------
% 17.73/3.54 % (510169)------------------------------
% 17.73/3.54 % (510178)------------------------------
% 17.73/3.54 % (510178)------------------------------
% 17.73/3.54 % (510185)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3900700614:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 17.73/3.54 % (510173)Refutation found. Thanks to Tanya!
% 17.73/3.54 % SZS status Unsatisfiable for theBenchmark
% 17.73/3.54 % SZS output start Proof for theBenchmark
% See solution above
% 18.53/3.79 % (510173)------------------------------
% 18.53/3.79 % (510173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/3.79 % (510173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/3.79 % (510173)CaDiCaL version: 2.1.3
% 18.53/3.79 % (510173)Termination reason: Refutation
% 18.53/3.79 % (510173)Time elapsed: 0.105 s
% 18.53/3.79 % (510173)Peak memory usage: 91 MB
% 18.53/3.79 % (510173)Instructions burned: 116 (million)
% 18.53/3.79 % (510173)------------------------------
% 18.53/3.79 % (510173)------------------------------
% 18.53/3.79 % (510091)Success in time 2.531 s
% 18.53/3.79 % Vampire exiting
%------------------------------------------------------------------------------