%------------------------------------------------------------------------------
% File : iProver-SAT---3.9.4
% Problem : MSC016+1 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p SAT
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:14:18 PM UTC 2026
% Result : CounterSatisfiable 7.59s 1.77s
% Output : Saturation 7.59s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
p(a,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abc) ).
fof(f2,axiom,
p(g(e,e),w,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gwb) ).
fof(f3,axiom,
p(h(d),g(a,c),g(b,b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hgg) ).
fof(f4,axiom,
p(h(d),g(e,e),k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hgk) ).
fof(f5,axiom,
p(k,lkg,hill),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',klh) ).
fof(f6,axiom,
p(a,a,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aaa) ).
fof(f7,axiom,
flower(lilly),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lilly) ).
fof(f8,axiom,
animal(pig),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pig) ).
fof(f9,axiom,
animal(horse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',horse) ).
fof(f10,axiom,
animal(cow),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cow) ).
fof(f11,axiom,
animal(pet(aparna)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pet) ).
fof(f12,axiom,
! [X0,X1] :
( ld__(X0,X1)
=> ld__(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__symmetry) ).
fof(f13,axiom,
ld__(aparna,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__aparna_a) ).
fof(f14,axiom,
ld__(cow,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__cow_a) ).
fof(f15,axiom,
ld__(horse,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__horse_a) ).
fof(f16,axiom,
ld__(lilly,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lilly_a) ).
fof(f17,axiom,
! [X0] : ld__(a,pet(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__a_pet) ).
fof(f18,axiom,
ld__(pig,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__pig_a) ).
fof(f19,axiom,
ld__(aparna,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__aparna_b) ).
fof(f20,axiom,
ld__(cow,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__cow_b) ).
fof(f21,axiom,
ld__(horse,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__horse_b) ).
fof(f22,axiom,
ld__(lilly,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lilly_b) ).
fof(f23,axiom,
! [X0] : ld__(b,pet(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__b_pet) ).
fof(f24,axiom,
ld__(pig,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__pig_b) ).
fof(f25,axiom,
ld__(aparna,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__aparna_c) ).
fof(f26,axiom,
ld__(cow,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__cow_c) ).
fof(f27,axiom,
ld__(horse,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__horse_c) ).
fof(f28,axiom,
ld__(lilly,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lilly_c) ).
fof(f29,axiom,
! [X0] : ld__(c,pet(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__c_pet) ).
fof(f30,axiom,
ld__(pig,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__pig_c) ).
fof(f31,axiom,
ld__(aparna,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__aparna_d) ).
fof(f32,axiom,
ld__(cow,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__cow_d) ).
fof(f33,axiom,
ld__(horse,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__horse_d) ).
fof(f34,axiom,
ld__(lilly,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lilly_d) ).
fof(f35,axiom,
! [X0] : ld__(d,pet(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__d_pet) ).
fof(f36,axiom,
ld__(pig,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__pig_d) ).
fof(f37,axiom,
ld__(aparna,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__aparna_e) ).
fof(f38,axiom,
ld__(cow,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__cow_e) ).
fof(f39,axiom,
ld__(horse,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__horse_e) ).
fof(f40,axiom,
ld__(lilly,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lilly_e) ).
fof(f41,axiom,
! [X0] : ld__(e,pet(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__e_pet) ).
fof(f42,axiom,
ld__(pig,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__pig_e) ).
fof(f43,axiom,
! [X0,X1] : ld__(aparna,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__aparna_g) ).
fof(f44,axiom,
! [X0,X1] : ld__(cow,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__cow_g) ).
fof(f45,axiom,
! [X0,X1] : ld__(horse,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__horse_g) ).
fof(f46,axiom,
! [X0,X1] : ld__(lilly,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lilly_g) ).
fof(f47,axiom,
! [X0,X1,X2] : ld__(pet(X2),g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__g_pet) ).
fof(f48,axiom,
! [X0,X1] : ld__(pig,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__pig_g) ).
fof(f49,axiom,
! [X0] : ld__(aparna,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__aparna_h) ).
fof(f50,axiom,
! [X0] : ld__(cow,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__cow_h) ).
fof(f51,axiom,
! [X0] : ld__(horse,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__horse_h) ).
fof(f52,axiom,
! [X0] : ld__(lilly,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lilly_h) ).
fof(f53,axiom,
! [X0,X1] : ld__(pet(X1),h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__h_pet) ).
fof(f54,axiom,
! [X0] : ld__(pig,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__pig_h) ).
fof(f55,axiom,
ld__(aparna,hill),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__aparna_hill) ).
fof(f56,axiom,
ld__(cow,hill),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__cow_hill) ).
fof(f57,axiom,
ld__(horse,hill),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__horse_hill) ).
fof(f58,axiom,
ld__(lilly,hill),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lilly_hill) ).
fof(f59,axiom,
! [X0] : ld__(hill,pet(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__hill_pet) ).
fof(f60,axiom,
ld__(pig,hill),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__pig_hill) ).
fof(f61,axiom,
ld__(aparna,k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__aparna_k) ).
fof(f62,axiom,
ld__(cow,k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__cow_k) ).
fof(f63,axiom,
ld__(horse,k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__horse_k) ).
fof(f64,axiom,
ld__(lilly,k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lilly_k) ).
fof(f65,axiom,
! [X0] : ld__(k,pet(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__k_pet) ).
fof(f66,axiom,
ld__(pig,k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__pig_k) ).
fof(f67,axiom,
ld__(aparna,lkg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__aparna_lkg) ).
fof(f68,axiom,
ld__(cow,lkg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__cow_lkg) ).
fof(f69,axiom,
ld__(horse,lkg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__horse_lkg) ).
fof(f70,axiom,
ld__(lilly,lkg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lilly_lkg) ).
fof(f71,axiom,
! [X0] : ld__(lkg,pet(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lkg_pet) ).
fof(f72,axiom,
ld__(pig,lkg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__pig_lkg) ).
fof(f73,axiom,
ld__(aparna,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__aparna_w) ).
fof(f74,axiom,
ld__(cow,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__cow_w) ).
fof(f75,axiom,
ld__(horse,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__horse_w) ).
fof(f76,axiom,
ld__(lilly,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lilly_w) ).
fof(f77,axiom,
! [X0] : ld__(w,pet(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__w_pet) ).
fof(f78,axiom,
ld__(pig,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__pig_w) ).
fof(f79,axiom,
! [X0,X1,X2,X3] :
( ( ld__(X2,X3)
| ld__(X0,X1) )
=> ld__(g(X0,X2),g(X1,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__g) ).
fof(f80,axiom,
! [X0,X1] :
( ld__(X0,X1)
=> ld__(h(X0),h(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__h) ).
fof(f81,axiom,
ld__(w,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__w_a) ).
fof(f82,axiom,
ld__(d,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__d_a) ).
fof(f83,axiom,
ld__(lkg,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lkg_a) ).
fof(f84,axiom,
ld__(a,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__a_c) ).
fof(f85,axiom,
! [X0] : ld__(a,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__a_h) ).
fof(f86,axiom,
ld__(k,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__k_a) ).
fof(f87,axiom,
ld__(hill,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__hill_a) ).
fof(f88,axiom,
ld__(e,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__e_a) ).
fof(f89,axiom,
! [X0,X1] : ld__(a,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__a_g) ).
fof(f90,axiom,
ld__(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__a_b) ).
fof(f91,axiom,
! [X0,X1] : ld__(b,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__b_g) ).
fof(f92,axiom,
ld__(k,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__k_b) ).
fof(f93,axiom,
ld__(w,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__w_b) ).
fof(f94,axiom,
ld__(d,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__d_b) ).
fof(f95,axiom,
ld__(hill,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__hill_b) ).
fof(f96,axiom,
! [X0] : ld__(b,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__b_h) ).
fof(f97,axiom,
ld__(e,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__e_b) ).
fof(f98,axiom,
ld__(b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__b_c) ).
fof(f99,axiom,
ld__(lkg,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lkg_b) ).
fof(f100,axiom,
ld__(w,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__w_c) ).
fof(f101,axiom,
! [X0,X1] : ld__(c,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__c_g) ).
fof(f102,axiom,
ld__(lkg,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lkg_c) ).
fof(f103,axiom,
ld__(e,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__e_c) ).
fof(f104,axiom,
ld__(d,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__d_c) ).
fof(f105,axiom,
ld__(k,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__k_c) ).
fof(f106,axiom,
! [X0] : ld__(c,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__c_h) ).
fof(f107,axiom,
ld__(hill,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__hill_c) ).
fof(f108,axiom,
ld__(lkg,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lkg_d) ).
fof(f109,axiom,
! [X0,X1] : ld__(d,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__d_g) ).
fof(f110,axiom,
ld__(k,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__k_d) ).
fof(f111,axiom,
ld__(hill,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__hill_d) ).
fof(f112,axiom,
ld__(d,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__d_w) ).
fof(f113,axiom,
! [X0] : ld__(d,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__d_h) ).
fof(f114,axiom,
ld__(d,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__d_e) ).
fof(f115,axiom,
! [X0] : ld__(e,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__e_h) ).
fof(f116,axiom,
ld__(e,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__e_w) ).
fof(f117,axiom,
! [X0,X1] : ld__(e,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__e_g) ).
fof(f118,axiom,
ld__(lkg,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lkg_e) ).
fof(f119,axiom,
ld__(hill,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__hill_e) ).
fof(f120,axiom,
ld__(k,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__k_e) ).
fof(f121,axiom,
! [X0,X1,X2] : ld__(h(X2),g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__g_h) ).
fof(f122,axiom,
! [X0,X1] : ld__(w,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__w_g) ).
fof(f123,axiom,
! [X0,X1] : ld__(k,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__k_g) ).
fof(f124,axiom,
! [X0,X1] : ld__(lkg,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lkg_g) ).
fof(f125,axiom,
! [X0,X1] : ld__(hill,g(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__hill_g) ).
fof(f126,axiom,
! [X0] : ld__(lkg,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lkg_h) ).
fof(f127,axiom,
! [X0] : ld__(hill,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__hill_h) ).
fof(f128,axiom,
! [X0] : ld__(w,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__w_h) ).
fof(f129,axiom,
! [X0] : ld__(k,h(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__k_h) ).
fof(f130,axiom,
ld__(lkg,hill),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lkg_hill) ).
fof(f131,axiom,
ld__(hill,k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__hill_k) ).
fof(f132,axiom,
ld__(hill,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__hill_w) ).
fof(f133,axiom,
ld__(k,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__k_w) ).
fof(f134,axiom,
ld__(lkg,k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lkg_k) ).
fof(f135,axiom,
ld__(lkg,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ld__lkg_w) ).
fof(f136,conjecture,
? [X0,X1,X2] :
( ( ld__(X2,a)
| ld__(X1,a)
| ld__(X0,a) )
& ( ld__(X2,g(b,b))
| ld__(X1,g(a,c))
| ld__(X0,h(d)) )
& ( ld__(X2,b)
| ld__(X1,w)
| ld__(X0,g(e,e)) )
& ( ld__(X2,c)
| ld__(X1,b)
| ld__(X0,a) )
& ( ld__(X2,k)
| ld__(X1,g(e,e))
| ld__(X0,h(d)) )
& ( ld__(X2,hill)
| ld__(X1,lkg)
| ld__(X0,k) )
& p(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_more_answers) ).
fof(f137,negated_conjecture,
~ ? [X0,X1,X2] :
( ( ld__(X2,a)
| ld__(X1,a)
| ld__(X0,a) )
& ( ld__(X2,g(b,b))
| ld__(X1,g(a,c))
| ld__(X0,h(d)) )
& ( ld__(X2,b)
| ld__(X1,w)
| ld__(X0,g(e,e)) )
& ( ld__(X2,c)
| ld__(X1,b)
| ld__(X0,a) )
& ( ld__(X2,k)
| ld__(X1,g(e,e))
| ld__(X0,h(d)) )
& ( ld__(X2,hill)
| ld__(X1,lkg)
| ld__(X0,k) )
& p(X0,X1,X2) ),
inference(negated_conjecture,[status(cth)],[f136]) ).
fof(f138,plain,
! [X0,X1] :
( ~ ld__(X0,X1)
| ld__(X1,X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f139,plain,
! [X0,X1,X2,X3] :
( ( ~ ld__(X2,X3)
& ~ ld__(X0,X1) )
| ld__(g(X0,X2),g(X1,X3)) ),
inference(ennf_transformation,[],[f79]) ).
fof(f140,plain,
! [X0,X1] :
( ~ ld__(X0,X1)
| ld__(h(X0),h(X1)) ),
inference(ennf_transformation,[],[f80]) ).
fof(f141,plain,
! [X0,X1,X2] :
( ( ~ ld__(X2,a)
& ~ ld__(X1,a)
& ~ ld__(X0,a) )
| ( ~ ld__(X2,g(b,b))
& ~ ld__(X1,g(a,c))
& ~ ld__(X0,h(d)) )
| ( ~ ld__(X2,b)
& ~ ld__(X1,w)
& ~ ld__(X0,g(e,e)) )
| ( ~ ld__(X2,c)
& ~ ld__(X1,b)
& ~ ld__(X0,a) )
| ( ~ ld__(X2,k)
& ~ ld__(X1,g(e,e))
& ~ ld__(X0,h(d)) )
| ( ~ ld__(X2,hill)
& ~ ld__(X1,lkg)
& ~ ld__(X0,k) )
| ~ p(X0,X1,X2) ),
inference(ennf_transformation,[],[f137]) ).
fof(f148,plain,
! [X0,X1,X2] :
( ~ sP4(X0,X1,X2)
| ( ~ ld__(X2,k)
& ~ ld__(X1,g(e,e))
& ~ ld__(X0,h(d)) ) ),
inference(nnf_transformation,[],[f146]) ).
fof(f149,plain,
! [X0,X1,X2] :
( ~ sP3(X0,X1,X2)
| ( ~ ld__(X2,c)
& ~ ld__(X1,b)
& ~ ld__(X0,a) ) ),
inference(nnf_transformation,[],[f145]) ).
fof(f150,plain,
! [X0,X1,X2] :
( ~ sP2(X0,X1,X2)
| ( ~ ld__(X2,b)
& ~ ld__(X1,w)
& ~ ld__(X0,g(e,e)) ) ),
inference(nnf_transformation,[],[f144]) ).
fof(f151,plain,
! [X0,X1,X2] :
( ~ sP1(X0,X1,X2)
| ( ~ ld__(X2,g(b,b))
& ~ ld__(X1,g(a,c))
& ~ ld__(X0,h(d)) ) ),
inference(nnf_transformation,[],[f143]) ).
fof(f153,plain,
p(a,b,c),
inference(cnf_transformation,[],[f1]) ).
fof(f154,plain,
p(g(e,e),w,b),
inference(cnf_transformation,[],[f2]) ).
fof(f155,plain,
p(h(d),g(a,c),g(b,b)),
inference(cnf_transformation,[],[f3]) ).
fof(f156,plain,
p(h(d),g(e,e),k),
inference(cnf_transformation,[],[f4]) ).
fof(f157,plain,
p(k,lkg,hill),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
p(a,a,a),
inference(cnf_transformation,[],[f6]) ).
fof(f159,plain,
flower(lilly),
inference(cnf_transformation,[],[f7]) ).
fof(f160,plain,
animal(pig),
inference(cnf_transformation,[],[f8]) ).
fof(f161,plain,
animal(horse),
inference(cnf_transformation,[],[f9]) ).
fof(f162,plain,
animal(cow),
inference(cnf_transformation,[],[f10]) ).
fof(f163,plain,
animal(pet(aparna)),
inference(cnf_transformation,[],[f11]) ).
fof(f164,plain,
! [X0,X1] :
( ~ ld__(X0,X1)
| ld__(X1,X0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f165,plain,
ld__(aparna,a),
inference(cnf_transformation,[],[f13]) ).
fof(f166,plain,
ld__(cow,a),
inference(cnf_transformation,[],[f14]) ).
fof(f167,plain,
ld__(horse,a),
inference(cnf_transformation,[],[f15]) ).
fof(f168,plain,
ld__(lilly,a),
inference(cnf_transformation,[],[f16]) ).
fof(f169,plain,
! [X0] : ld__(a,pet(X0)),
inference(cnf_transformation,[],[f17]) ).
fof(f170,plain,
ld__(pig,a),
inference(cnf_transformation,[],[f18]) ).
fof(f171,plain,
ld__(aparna,b),
inference(cnf_transformation,[],[f19]) ).
fof(f172,plain,
ld__(cow,b),
inference(cnf_transformation,[],[f20]) ).
fof(f173,plain,
ld__(horse,b),
inference(cnf_transformation,[],[f21]) ).
fof(f174,plain,
ld__(lilly,b),
inference(cnf_transformation,[],[f22]) ).
fof(f175,plain,
! [X0] : ld__(b,pet(X0)),
inference(cnf_transformation,[],[f23]) ).
fof(f176,plain,
ld__(pig,b),
inference(cnf_transformation,[],[f24]) ).
fof(f177,plain,
ld__(aparna,c),
inference(cnf_transformation,[],[f25]) ).
fof(f178,plain,
ld__(cow,c),
inference(cnf_transformation,[],[f26]) ).
fof(f179,plain,
ld__(horse,c),
inference(cnf_transformation,[],[f27]) ).
fof(f180,plain,
ld__(lilly,c),
inference(cnf_transformation,[],[f28]) ).
fof(f181,plain,
! [X0] : ld__(c,pet(X0)),
inference(cnf_transformation,[],[f29]) ).
fof(f182,plain,
ld__(pig,c),
inference(cnf_transformation,[],[f30]) ).
fof(f183,plain,
ld__(aparna,d),
inference(cnf_transformation,[],[f31]) ).
fof(f184,plain,
ld__(cow,d),
inference(cnf_transformation,[],[f32]) ).
fof(f185,plain,
ld__(horse,d),
inference(cnf_transformation,[],[f33]) ).
fof(f186,plain,
ld__(lilly,d),
inference(cnf_transformation,[],[f34]) ).
fof(f187,plain,
! [X0] : ld__(d,pet(X0)),
inference(cnf_transformation,[],[f35]) ).
fof(f188,plain,
ld__(pig,d),
inference(cnf_transformation,[],[f36]) ).
fof(f189,plain,
ld__(aparna,e),
inference(cnf_transformation,[],[f37]) ).
fof(f190,plain,
ld__(cow,e),
inference(cnf_transformation,[],[f38]) ).
fof(f191,plain,
ld__(horse,e),
inference(cnf_transformation,[],[f39]) ).
fof(f192,plain,
ld__(lilly,e),
inference(cnf_transformation,[],[f40]) ).
fof(f193,plain,
! [X0] : ld__(e,pet(X0)),
inference(cnf_transformation,[],[f41]) ).
fof(f194,plain,
ld__(pig,e),
inference(cnf_transformation,[],[f42]) ).
fof(f195,plain,
! [X0,X1] : ld__(aparna,g(X0,X1)),
inference(cnf_transformation,[],[f43]) ).
fof(f196,plain,
! [X0,X1] : ld__(cow,g(X0,X1)),
inference(cnf_transformation,[],[f44]) ).
fof(f197,plain,
! [X0,X1] : ld__(horse,g(X0,X1)),
inference(cnf_transformation,[],[f45]) ).
fof(f198,plain,
! [X0,X1] : ld__(lilly,g(X0,X1)),
inference(cnf_transformation,[],[f46]) ).
fof(f199,plain,
! [X2,X0,X1] : ld__(pet(X2),g(X0,X1)),
inference(cnf_transformation,[],[f47]) ).
fof(f200,plain,
! [X0,X1] : ld__(pig,g(X0,X1)),
inference(cnf_transformation,[],[f48]) ).
fof(f201,plain,
! [X0] : ld__(aparna,h(X0)),
inference(cnf_transformation,[],[f49]) ).
fof(f202,plain,
! [X0] : ld__(cow,h(X0)),
inference(cnf_transformation,[],[f50]) ).
fof(f203,plain,
! [X0] : ld__(horse,h(X0)),
inference(cnf_transformation,[],[f51]) ).
fof(f204,plain,
! [X0] : ld__(lilly,h(X0)),
inference(cnf_transformation,[],[f52]) ).
fof(f205,plain,
! [X0,X1] : ld__(pet(X1),h(X0)),
inference(cnf_transformation,[],[f53]) ).
fof(f206,plain,
! [X0] : ld__(pig,h(X0)),
inference(cnf_transformation,[],[f54]) ).
fof(f207,plain,
ld__(aparna,hill),
inference(cnf_transformation,[],[f55]) ).
fof(f208,plain,
ld__(cow,hill),
inference(cnf_transformation,[],[f56]) ).
fof(f209,plain,
ld__(horse,hill),
inference(cnf_transformation,[],[f57]) ).
fof(f210,plain,
ld__(lilly,hill),
inference(cnf_transformation,[],[f58]) ).
fof(f211,plain,
! [X0] : ld__(hill,pet(X0)),
inference(cnf_transformation,[],[f59]) ).
fof(f212,plain,
ld__(pig,hill),
inference(cnf_transformation,[],[f60]) ).
fof(f213,plain,
ld__(aparna,k),
inference(cnf_transformation,[],[f61]) ).
fof(f214,plain,
ld__(cow,k),
inference(cnf_transformation,[],[f62]) ).
fof(f215,plain,
ld__(horse,k),
inference(cnf_transformation,[],[f63]) ).
fof(f216,plain,
ld__(lilly,k),
inference(cnf_transformation,[],[f64]) ).
fof(f217,plain,
! [X0] : ld__(k,pet(X0)),
inference(cnf_transformation,[],[f65]) ).
fof(f218,plain,
ld__(pig,k),
inference(cnf_transformation,[],[f66]) ).
fof(f219,plain,
ld__(aparna,lkg),
inference(cnf_transformation,[],[f67]) ).
fof(f220,plain,
ld__(cow,lkg),
inference(cnf_transformation,[],[f68]) ).
fof(f221,plain,
ld__(horse,lkg),
inference(cnf_transformation,[],[f69]) ).
fof(f222,plain,
ld__(lilly,lkg),
inference(cnf_transformation,[],[f70]) ).
fof(f223,plain,
! [X0] : ld__(lkg,pet(X0)),
inference(cnf_transformation,[],[f71]) ).
fof(f224,plain,
ld__(pig,lkg),
inference(cnf_transformation,[],[f72]) ).
fof(f225,plain,
ld__(aparna,w),
inference(cnf_transformation,[],[f73]) ).
fof(f226,plain,
ld__(cow,w),
inference(cnf_transformation,[],[f74]) ).
fof(f227,plain,
ld__(horse,w),
inference(cnf_transformation,[],[f75]) ).
fof(f228,plain,
ld__(lilly,w),
inference(cnf_transformation,[],[f76]) ).
fof(f229,plain,
! [X0] : ld__(w,pet(X0)),
inference(cnf_transformation,[],[f77]) ).
fof(f230,plain,
ld__(pig,w),
inference(cnf_transformation,[],[f78]) ).
fof(f231,plain,
! [X2,X3,X0,X1] :
( ~ ld__(X2,X3)
| ld__(g(X0,X2),g(X1,X3)) ),
inference(cnf_transformation,[],[f139]) ).
fof(f232,plain,
! [X2,X3,X0,X1] :
( ~ ld__(X0,X1)
| ld__(g(X0,X2),g(X1,X3)) ),
inference(cnf_transformation,[],[f139]) ).
fof(f233,plain,
! [X0,X1] :
( ~ ld__(X0,X1)
| ld__(h(X0),h(X1)) ),
inference(cnf_transformation,[],[f140]) ).
fof(f234,plain,
ld__(w,a),
inference(cnf_transformation,[],[f81]) ).
fof(f235,plain,
ld__(d,a),
inference(cnf_transformation,[],[f82]) ).
fof(f236,plain,
ld__(lkg,a),
inference(cnf_transformation,[],[f83]) ).
fof(f237,plain,
ld__(a,c),
inference(cnf_transformation,[],[f84]) ).
fof(f238,plain,
! [X0] : ld__(a,h(X0)),
inference(cnf_transformation,[],[f85]) ).
fof(f239,plain,
ld__(k,a),
inference(cnf_transformation,[],[f86]) ).
fof(f240,plain,
ld__(hill,a),
inference(cnf_transformation,[],[f87]) ).
fof(f241,plain,
ld__(e,a),
inference(cnf_transformation,[],[f88]) ).
fof(f242,plain,
! [X0,X1] : ld__(a,g(X0,X1)),
inference(cnf_transformation,[],[f89]) ).
fof(f243,plain,
ld__(a,b),
inference(cnf_transformation,[],[f90]) ).
fof(f244,plain,
! [X0,X1] : ld__(b,g(X0,X1)),
inference(cnf_transformation,[],[f91]) ).
fof(f245,plain,
ld__(k,b),
inference(cnf_transformation,[],[f92]) ).
fof(f246,plain,
ld__(w,b),
inference(cnf_transformation,[],[f93]) ).
fof(f247,plain,
ld__(d,b),
inference(cnf_transformation,[],[f94]) ).
fof(f248,plain,
ld__(hill,b),
inference(cnf_transformation,[],[f95]) ).
fof(f249,plain,
! [X0] : ld__(b,h(X0)),
inference(cnf_transformation,[],[f96]) ).
fof(f250,plain,
ld__(e,b),
inference(cnf_transformation,[],[f97]) ).
fof(f251,plain,
ld__(b,c),
inference(cnf_transformation,[],[f98]) ).
fof(f252,plain,
ld__(lkg,b),
inference(cnf_transformation,[],[f99]) ).
fof(f253,plain,
ld__(w,c),
inference(cnf_transformation,[],[f100]) ).
fof(f254,plain,
! [X0,X1] : ld__(c,g(X0,X1)),
inference(cnf_transformation,[],[f101]) ).
fof(f255,plain,
ld__(lkg,c),
inference(cnf_transformation,[],[f102]) ).
fof(f256,plain,
ld__(e,c),
inference(cnf_transformation,[],[f103]) ).
fof(f257,plain,
ld__(d,c),
inference(cnf_transformation,[],[f104]) ).
fof(f258,plain,
ld__(k,c),
inference(cnf_transformation,[],[f105]) ).
fof(f259,plain,
! [X0] : ld__(c,h(X0)),
inference(cnf_transformation,[],[f106]) ).
fof(f260,plain,
ld__(hill,c),
inference(cnf_transformation,[],[f107]) ).
fof(f261,plain,
ld__(lkg,d),
inference(cnf_transformation,[],[f108]) ).
fof(f262,plain,
! [X0,X1] : ld__(d,g(X0,X1)),
inference(cnf_transformation,[],[f109]) ).
fof(f263,plain,
ld__(k,d),
inference(cnf_transformation,[],[f110]) ).
fof(f264,plain,
ld__(hill,d),
inference(cnf_transformation,[],[f111]) ).
fof(f265,plain,
ld__(d,w),
inference(cnf_transformation,[],[f112]) ).
fof(f266,plain,
! [X0] : ld__(d,h(X0)),
inference(cnf_transformation,[],[f113]) ).
fof(f267,plain,
ld__(d,e),
inference(cnf_transformation,[],[f114]) ).
fof(f268,plain,
! [X0] : ld__(e,h(X0)),
inference(cnf_transformation,[],[f115]) ).
fof(f269,plain,
ld__(e,w),
inference(cnf_transformation,[],[f116]) ).
fof(f270,plain,
! [X0,X1] : ld__(e,g(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f271,plain,
ld__(lkg,e),
inference(cnf_transformation,[],[f118]) ).
fof(f272,plain,
ld__(hill,e),
inference(cnf_transformation,[],[f119]) ).
fof(f273,plain,
ld__(k,e),
inference(cnf_transformation,[],[f120]) ).
fof(f274,plain,
! [X2,X0,X1] : ld__(h(X2),g(X0,X1)),
inference(cnf_transformation,[],[f121]) ).
fof(f275,plain,
! [X0,X1] : ld__(w,g(X0,X1)),
inference(cnf_transformation,[],[f122]) ).
fof(f276,plain,
! [X0,X1] : ld__(k,g(X0,X1)),
inference(cnf_transformation,[],[f123]) ).
fof(f277,plain,
! [X0,X1] : ld__(lkg,g(X0,X1)),
inference(cnf_transformation,[],[f124]) ).
fof(f278,plain,
! [X0,X1] : ld__(hill,g(X0,X1)),
inference(cnf_transformation,[],[f125]) ).
fof(f279,plain,
! [X0] : ld__(lkg,h(X0)),
inference(cnf_transformation,[],[f126]) ).
fof(f280,plain,
! [X0] : ld__(hill,h(X0)),
inference(cnf_transformation,[],[f127]) ).
fof(f281,plain,
! [X0] : ld__(w,h(X0)),
inference(cnf_transformation,[],[f128]) ).
fof(f282,plain,
! [X0] : ld__(k,h(X0)),
inference(cnf_transformation,[],[f129]) ).
fof(f283,plain,
ld__(lkg,hill),
inference(cnf_transformation,[],[f130]) ).
fof(f284,plain,
ld__(hill,k),
inference(cnf_transformation,[],[f131]) ).
fof(f285,plain,
ld__(hill,w),
inference(cnf_transformation,[],[f132]) ).
fof(f286,plain,
ld__(k,w),
inference(cnf_transformation,[],[f133]) ).
fof(f287,plain,
ld__(lkg,k),
inference(cnf_transformation,[],[f134]) ).
fof(f288,plain,
ld__(lkg,w),
inference(cnf_transformation,[],[f135]) ).
fof(f289,plain,
! [X2,X0,X1] :
( ~ sP4(X0,X1,X2)
| ~ ld__(X2,k) ),
inference(cnf_transformation,[],[f148]) ).
fof(f290,plain,
! [X2,X0,X1] :
( ~ sP4(X0,X1,X2)
| ~ ld__(X1,g(e,e)) ),
inference(cnf_transformation,[],[f148]) ).
fof(f291,plain,
! [X2,X0,X1] :
( ~ sP4(X0,X1,X2)
| ~ ld__(X0,h(d)) ),
inference(cnf_transformation,[],[f148]) ).
fof(f292,plain,
! [X2,X0,X1] :
( ~ sP3(X0,X1,X2)
| ~ ld__(X2,c) ),
inference(cnf_transformation,[],[f149]) ).
fof(f293,plain,
! [X2,X0,X1] :
( ~ sP3(X0,X1,X2)
| ~ ld__(X1,b) ),
inference(cnf_transformation,[],[f149]) ).
fof(f294,plain,
! [X2,X0,X1] :
( ~ sP3(X0,X1,X2)
| ~ ld__(X0,a) ),
inference(cnf_transformation,[],[f149]) ).
fof(f295,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,X2)
| ~ ld__(X2,b) ),
inference(cnf_transformation,[],[f150]) ).
fof(f296,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,X2)
| ~ ld__(X1,w) ),
inference(cnf_transformation,[],[f150]) ).
fof(f297,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1,X2)
| ~ ld__(X0,g(e,e)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f298,plain,
! [X2,X0,X1] :
( ~ sP1(X0,X1,X2)
| ~ ld__(X2,g(b,b)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f299,plain,
! [X2,X0,X1] :
( ~ sP1(X0,X1,X2)
| ~ ld__(X1,g(a,c)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f300,plain,
! [X2,X0,X1] :
( ~ sP1(X0,X1,X2)
| ~ ld__(X0,h(d)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f304,plain,
! [X2,X0,X1] :
( sP0(X0,X1,X2)
| sP1(X0,X1,X2)
| sP2(X0,X1,X2)
| sP3(X0,X1,X2)
| sP4(X0,X1,X2)
| ~ ld__(X2,hill)
| ~ p(X0,X1,X2) ),
inference(cnf_transformation,[],[f147]) ).
fof(f305,plain,
! [X2,X0,X1] :
( sP0(X0,X1,X2)
| sP1(X0,X1,X2)
| sP2(X0,X1,X2)
| sP3(X0,X1,X2)
| sP4(X0,X1,X2)
| ~ ld__(X1,lkg)
| ~ p(X0,X1,X2) ),
inference(cnf_transformation,[],[f147]) ).
fof(f306,plain,
! [X2,X0,X1] :
( sP0(X0,X1,X2)
| sP1(X0,X1,X2)
| sP2(X0,X1,X2)
| sP3(X0,X1,X2)
| sP4(X0,X1,X2)
| ~ ld__(X0,k)
| ~ p(X0,X1,X2) ),
inference(cnf_transformation,[],[f147]) ).
tcf(c_49,plain,
p(a,b,c),
inference(cnf_transformation,[],[f153]) ).
tcf(c_50,plain,
p(g(e,e),w,b),
inference(cnf_transformation,[],[f154]) ).
tcf(c_51,plain,
p(h(d),g(a,c),g(b,b)),
inference(cnf_transformation,[],[f155]) ).
tcf(c_52,plain,
p(h(d),g(e,e),k),
inference(cnf_transformation,[],[f156]) ).
tcf(c_53,plain,
p(k,lkg,hill),
inference(cnf_transformation,[],[f157]) ).
tcf(c_54,plain,
p(a,a,a),
inference(cnf_transformation,[],[f158]) ).
tcf(c_55,plain,
flower(lilly),
inference(cnf_transformation,[],[f159]) ).
tcf(c_56,plain,
animal(pig),
inference(cnf_transformation,[],[f160]) ).
tcf(c_57,plain,
animal(horse),
inference(cnf_transformation,[],[f161]) ).
tcf(c_58,plain,
animal(cow),
inference(cnf_transformation,[],[f162]) ).
tcf(c_59,plain,
animal(pet(aparna)),
inference(cnf_transformation,[],[f163]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( ld__(X1,X0)
| ~ ld__(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_61,plain,
ld__(aparna,a),
inference(cnf_transformation,[],[f165]) ).
tcf(c_62,plain,
ld__(cow,a),
inference(cnf_transformation,[],[f166]) ).
tcf(c_63,plain,
ld__(horse,a),
inference(cnf_transformation,[],[f167]) ).
tcf(c_64,plain,
ld__(lilly,a),
inference(cnf_transformation,[],[f168]) ).
tcf(c_65,plain,
! [X0: $i] : ld__(a,pet(X0)),
inference(cnf_transformation,[],[f169]) ).
tcf(c_66,plain,
ld__(pig,a),
inference(cnf_transformation,[],[f170]) ).
tcf(c_67,plain,
ld__(aparna,b),
inference(cnf_transformation,[],[f171]) ).
tcf(c_68,plain,
ld__(cow,b),
inference(cnf_transformation,[],[f172]) ).
tcf(c_69,plain,
ld__(horse,b),
inference(cnf_transformation,[],[f173]) ).
tcf(c_70,plain,
ld__(lilly,b),
inference(cnf_transformation,[],[f174]) ).
tcf(c_71,plain,
! [X0: $i] : ld__(b,pet(X0)),
inference(cnf_transformation,[],[f175]) ).
tcf(c_72,plain,
ld__(pig,b),
inference(cnf_transformation,[],[f176]) ).
tcf(c_73,plain,
ld__(aparna,c),
inference(cnf_transformation,[],[f177]) ).
tcf(c_74,plain,
ld__(cow,c),
inference(cnf_transformation,[],[f178]) ).
tcf(c_75,plain,
ld__(horse,c),
inference(cnf_transformation,[],[f179]) ).
tcf(c_76,plain,
ld__(lilly,c),
inference(cnf_transformation,[],[f180]) ).
tcf(c_77,plain,
! [X0: $i] : ld__(c,pet(X0)),
inference(cnf_transformation,[],[f181]) ).
tcf(c_78,plain,
ld__(pig,c),
inference(cnf_transformation,[],[f182]) ).
tcf(c_79,plain,
ld__(aparna,d),
inference(cnf_transformation,[],[f183]) ).
tcf(c_80,plain,
ld__(cow,d),
inference(cnf_transformation,[],[f184]) ).
tcf(c_81,plain,
ld__(horse,d),
inference(cnf_transformation,[],[f185]) ).
tcf(c_82,plain,
ld__(lilly,d),
inference(cnf_transformation,[],[f186]) ).
tcf(c_83,plain,
! [X0: $i] : ld__(d,pet(X0)),
inference(cnf_transformation,[],[f187]) ).
tcf(c_84,plain,
ld__(pig,d),
inference(cnf_transformation,[],[f188]) ).
tcf(c_85,plain,
ld__(aparna,e),
inference(cnf_transformation,[],[f189]) ).
tcf(c_86,plain,
ld__(cow,e),
inference(cnf_transformation,[],[f190]) ).
tcf(c_87,plain,
ld__(horse,e),
inference(cnf_transformation,[],[f191]) ).
tcf(c_88,plain,
ld__(lilly,e),
inference(cnf_transformation,[],[f192]) ).
tcf(c_89,plain,
! [X0: $i] : ld__(e,pet(X0)),
inference(cnf_transformation,[],[f193]) ).
tcf(c_90,plain,
ld__(pig,e),
inference(cnf_transformation,[],[f194]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] : ld__(aparna,g(X0,X1)),
inference(cnf_transformation,[],[f195]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] : ld__(cow,g(X0,X1)),
inference(cnf_transformation,[],[f196]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] : ld__(horse,g(X0,X1)),
inference(cnf_transformation,[],[f197]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i] : ld__(lilly,g(X0,X1)),
inference(cnf_transformation,[],[f198]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i] : ld__(pet(X0),g(X1,X2)),
inference(cnf_transformation,[],[f199]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i] : ld__(pig,g(X0,X1)),
inference(cnf_transformation,[],[f200]) ).
tcf(c_97,plain,
! [X0: $i] : ld__(aparna,h(X0)),
inference(cnf_transformation,[],[f201]) ).
tcf(c_98,plain,
! [X0: $i] : ld__(cow,h(X0)),
inference(cnf_transformation,[],[f202]) ).
tcf(c_99,plain,
! [X0: $i] : ld__(horse,h(X0)),
inference(cnf_transformation,[],[f203]) ).
tcf(c_100,plain,
! [X0: $i] : ld__(lilly,h(X0)),
inference(cnf_transformation,[],[f204]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i] : ld__(pet(X0),h(X1)),
inference(cnf_transformation,[],[f205]) ).
tcf(c_102,plain,
! [X0: $i] : ld__(pig,h(X0)),
inference(cnf_transformation,[],[f206]) ).
tcf(c_103,plain,
ld__(aparna,hill),
inference(cnf_transformation,[],[f207]) ).
tcf(c_104,plain,
ld__(cow,hill),
inference(cnf_transformation,[],[f208]) ).
tcf(c_105,plain,
ld__(horse,hill),
inference(cnf_transformation,[],[f209]) ).
tcf(c_106,plain,
ld__(lilly,hill),
inference(cnf_transformation,[],[f210]) ).
tcf(c_107,plain,
! [X0: $i] : ld__(hill,pet(X0)),
inference(cnf_transformation,[],[f211]) ).
tcf(c_108,plain,
ld__(pig,hill),
inference(cnf_transformation,[],[f212]) ).
tcf(c_109,plain,
ld__(aparna,k),
inference(cnf_transformation,[],[f213]) ).
tcf(c_110,plain,
ld__(cow,k),
inference(cnf_transformation,[],[f214]) ).
tcf(c_111,plain,
ld__(horse,k),
inference(cnf_transformation,[],[f215]) ).
tcf(c_112,plain,
ld__(lilly,k),
inference(cnf_transformation,[],[f216]) ).
tcf(c_113,plain,
! [X0: $i] : ld__(k,pet(X0)),
inference(cnf_transformation,[],[f217]) ).
tcf(c_114,plain,
ld__(pig,k),
inference(cnf_transformation,[],[f218]) ).
tcf(c_115,plain,
ld__(aparna,lkg),
inference(cnf_transformation,[],[f219]) ).
tcf(c_116,plain,
ld__(cow,lkg),
inference(cnf_transformation,[],[f220]) ).
tcf(c_117,plain,
ld__(horse,lkg),
inference(cnf_transformation,[],[f221]) ).
tcf(c_118,plain,
ld__(lilly,lkg),
inference(cnf_transformation,[],[f222]) ).
tcf(c_119,plain,
! [X0: $i] : ld__(lkg,pet(X0)),
inference(cnf_transformation,[],[f223]) ).
tcf(c_120,plain,
ld__(pig,lkg),
inference(cnf_transformation,[],[f224]) ).
tcf(c_121,plain,
ld__(aparna,w),
inference(cnf_transformation,[],[f225]) ).
tcf(c_122,plain,
ld__(cow,w),
inference(cnf_transformation,[],[f226]) ).
tcf(c_123,plain,
ld__(horse,w),
inference(cnf_transformation,[],[f227]) ).
tcf(c_124,plain,
ld__(lilly,w),
inference(cnf_transformation,[],[f228]) ).
tcf(c_125,plain,
! [X0: $i] : ld__(w,pet(X0)),
inference(cnf_transformation,[],[f229]) ).
tcf(c_126,plain,
ld__(pig,w),
inference(cnf_transformation,[],[f230]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ld__(g(X0,X2),g(X1,X3))
| ~ ld__(X0,X1) ),
inference(cnf_transformation,[],[f232]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ld__(g(X2,X0),g(X3,X1))
| ~ ld__(X0,X1) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i] :
( ld__(h(X0),h(X1))
| ~ ld__(X0,X1) ),
inference(cnf_transformation,[],[f233]) ).
tcf(c_130,plain,
ld__(w,a),
inference(cnf_transformation,[],[f234]) ).
tcf(c_131,plain,
ld__(d,a),
inference(cnf_transformation,[],[f235]) ).
tcf(c_132,plain,
ld__(lkg,a),
inference(cnf_transformation,[],[f236]) ).
tcf(c_133,plain,
ld__(a,c),
inference(cnf_transformation,[],[f237]) ).
tcf(c_134,plain,
! [X0: $i] : ld__(a,h(X0)),
inference(cnf_transformation,[],[f238]) ).
tcf(c_135,plain,
ld__(k,a),
inference(cnf_transformation,[],[f239]) ).
tcf(c_136,plain,
ld__(hill,a),
inference(cnf_transformation,[],[f240]) ).
tcf(c_137,plain,
ld__(e,a),
inference(cnf_transformation,[],[f241]) ).
tcf(c_138,plain,
! [X0: $i,X1: $i] : ld__(a,g(X0,X1)),
inference(cnf_transformation,[],[f242]) ).
tcf(c_139,plain,
ld__(a,b),
inference(cnf_transformation,[],[f243]) ).
tcf(c_140,plain,
! [X0: $i,X1: $i] : ld__(b,g(X0,X1)),
inference(cnf_transformation,[],[f244]) ).
tcf(c_141,plain,
ld__(k,b),
inference(cnf_transformation,[],[f245]) ).
tcf(c_142,plain,
ld__(w,b),
inference(cnf_transformation,[],[f246]) ).
tcf(c_143,plain,
ld__(d,b),
inference(cnf_transformation,[],[f247]) ).
tcf(c_144,plain,
ld__(hill,b),
inference(cnf_transformation,[],[f248]) ).
tcf(c_145,plain,
! [X0: $i] : ld__(b,h(X0)),
inference(cnf_transformation,[],[f249]) ).
tcf(c_146,plain,
ld__(e,b),
inference(cnf_transformation,[],[f250]) ).
tcf(c_147,plain,
ld__(b,c),
inference(cnf_transformation,[],[f251]) ).
tcf(c_148,plain,
ld__(lkg,b),
inference(cnf_transformation,[],[f252]) ).
tcf(c_149,plain,
ld__(w,c),
inference(cnf_transformation,[],[f253]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i] : ld__(c,g(X0,X1)),
inference(cnf_transformation,[],[f254]) ).
tcf(c_151,plain,
ld__(lkg,c),
inference(cnf_transformation,[],[f255]) ).
tcf(c_152,plain,
ld__(e,c),
inference(cnf_transformation,[],[f256]) ).
tcf(c_153,plain,
ld__(d,c),
inference(cnf_transformation,[],[f257]) ).
tcf(c_154,plain,
ld__(k,c),
inference(cnf_transformation,[],[f258]) ).
tcf(c_155,plain,
! [X0: $i] : ld__(c,h(X0)),
inference(cnf_transformation,[],[f259]) ).
tcf(c_156,plain,
ld__(hill,c),
inference(cnf_transformation,[],[f260]) ).
tcf(c_157,plain,
ld__(lkg,d),
inference(cnf_transformation,[],[f261]) ).
tcf(c_158,plain,
! [X0: $i,X1: $i] : ld__(d,g(X0,X1)),
inference(cnf_transformation,[],[f262]) ).
tcf(c_159,plain,
ld__(k,d),
inference(cnf_transformation,[],[f263]) ).
tcf(c_160,plain,
ld__(hill,d),
inference(cnf_transformation,[],[f264]) ).
tcf(c_161,plain,
ld__(d,w),
inference(cnf_transformation,[],[f265]) ).
tcf(c_162,plain,
! [X0: $i] : ld__(d,h(X0)),
inference(cnf_transformation,[],[f266]) ).
tcf(c_163,plain,
ld__(d,e),
inference(cnf_transformation,[],[f267]) ).
tcf(c_164,plain,
! [X0: $i] : ld__(e,h(X0)),
inference(cnf_transformation,[],[f268]) ).
tcf(c_165,plain,
ld__(e,w),
inference(cnf_transformation,[],[f269]) ).
tcf(c_166,plain,
! [X0: $i,X1: $i] : ld__(e,g(X0,X1)),
inference(cnf_transformation,[],[f270]) ).
tcf(c_167,plain,
ld__(lkg,e),
inference(cnf_transformation,[],[f271]) ).
tcf(c_168,plain,
ld__(hill,e),
inference(cnf_transformation,[],[f272]) ).
tcf(c_169,plain,
ld__(k,e),
inference(cnf_transformation,[],[f273]) ).
tcf(c_170,plain,
! [X0: $i,X1: $i,X2: $i] : ld__(h(X0),g(X1,X2)),
inference(cnf_transformation,[],[f274]) ).
tcf(c_171,plain,
! [X0: $i,X1: $i] : ld__(w,g(X0,X1)),
inference(cnf_transformation,[],[f275]) ).
tcf(c_172,plain,
! [X0: $i,X1: $i] : ld__(k,g(X0,X1)),
inference(cnf_transformation,[],[f276]) ).
tcf(c_173,plain,
! [X0: $i,X1: $i] : ld__(lkg,g(X0,X1)),
inference(cnf_transformation,[],[f277]) ).
tcf(c_174,plain,
! [X0: $i,X1: $i] : ld__(hill,g(X0,X1)),
inference(cnf_transformation,[],[f278]) ).
tcf(c_175,plain,
! [X0: $i] : ld__(lkg,h(X0)),
inference(cnf_transformation,[],[f279]) ).
tcf(c_176,plain,
! [X0: $i] : ld__(hill,h(X0)),
inference(cnf_transformation,[],[f280]) ).
tcf(c_177,plain,
! [X0: $i] : ld__(w,h(X0)),
inference(cnf_transformation,[],[f281]) ).
tcf(c_178,plain,
! [X0: $i] : ld__(k,h(X0)),
inference(cnf_transformation,[],[f282]) ).
tcf(c_179,plain,
ld__(lkg,hill),
inference(cnf_transformation,[],[f283]) ).
tcf(c_180,plain,
ld__(hill,k),
inference(cnf_transformation,[],[f284]) ).
tcf(c_181,plain,
ld__(hill,w),
inference(cnf_transformation,[],[f285]) ).
tcf(c_182,plain,
ld__(k,w),
inference(cnf_transformation,[],[f286]) ).
tcf(c_183,plain,
ld__(lkg,k),
inference(cnf_transformation,[],[f287]) ).
tcf(c_184,plain,
ld__(lkg,w),
inference(cnf_transformation,[],[f288]) ).
tcf(c_185,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X0,h(d))
| ~ sP4(X0,X1,X2) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_186,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sP4(X1,X0,X2)
| ~ ld__(X0,g(e,e)) ),
inference(cnf_transformation,[],[f290]) ).
tcf(c_187,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X2,k)
| ~ sP4(X0,X1,X2) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_188,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X0,a)
| ~ sP3(X0,X1,X2) ),
inference(cnf_transformation,[],[f294]) ).
tcf(c_189,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X1,b)
| ~ sP3(X0,X1,X2) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_190,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X2,c)
| ~ sP3(X0,X1,X2) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_191,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sP2(X0,X1,X2)
| ~ ld__(X0,g(e,e)) ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_192,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X1,w)
| ~ sP2(X0,X1,X2) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_193,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X2,b)
| ~ sP2(X0,X1,X2) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_194,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X0,h(d))
| ~ sP1(X0,X1,X2) ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_195,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sP1(X1,X0,X2)
| ~ ld__(X0,g(a,c)) ),
inference(cnf_transformation,[],[f299]) ).
tcf(c_196,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sP1(X1,X2,X0)
| ~ ld__(X0,g(b,b)) ),
inference(cnf_transformation,[],[f298]) ).
tcf(c_200,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP0(X0,X1,X2)
| sP1(X0,X1,X2)
| sP2(X0,X1,X2)
| sP3(X0,X1,X2)
| sP4(X0,X1,X2)
| ~ ld__(X0,k)
| ~ p(X0,X1,X2) ),
inference(cnf_transformation,[],[f306]) ).
tcf(c_201,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP0(X0,X1,X2)
| sP1(X0,X1,X2)
| sP2(X0,X1,X2)
| sP3(X0,X1,X2)
| sP4(X0,X1,X2)
| ~ ld__(X1,lkg)
| ~ p(X0,X1,X2) ),
inference(cnf_transformation,[],[f305]) ).
tcf(c_202,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP0(X0,X1,X2)
| sP1(X0,X1,X2)
| sP2(X0,X1,X2)
| sP3(X0,X1,X2)
| sP4(X0,X1,X2)
| ~ ld__(X2,hill)
| ~ p(X0,X1,X2) ),
inference(cnf_transformation,[],[f304]) ).
tcf(c_244,plain,
( ~ ld__(a,b)
| ~ sP2(a,a,a) ),
inference(instantiation,[status(thm)],[c_193]) ).
tcf(c_246,plain,
( ~ ld__(a,c)
| ~ sP3(a,a,a) ),
inference(instantiation,[status(thm)],[c_190]) ).
tcf(c_249,plain,
( ~ ld__(a,k)
| ~ sP4(a,a,a) ),
inference(instantiation,[status(thm)],[c_187]) ).
tcf(c_251,plain,
( ~ sP1(a,a,a)
| ~ ld__(a,h(d)) ),
inference(instantiation,[status(thm)],[c_194]) ).
tcf(c_258,plain,
( sP0(a,a,a)
| sP1(a,a,a)
| sP2(a,a,a)
| sP3(a,a,a)
| sP4(a,a,a)
| ~ ld__(a,hill)
| ~ p(a,a,a) ),
inference(instantiation,[status(thm)],[c_202]) ).
tcf(c_390,plain,
( ld__(a,k)
| ~ ld__(k,a) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_391,plain,
( ld__(a,hill)
| ~ ld__(hill,a) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_401,plain,
( ld__(b,hill)
| ~ ld__(hill,b) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_453,plain,
( ld__(k,hill)
| ~ ld__(hill,k) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_639,plain,
ld__(a,h(d)),
inference(instantiation,[status(thm)],[c_134]) ).
tcf(c_1515,plain,
( sP0(a,b,c)
| sP1(a,b,c)
| sP2(a,b,c)
| sP3(a,b,c)
| sP4(a,b,c)
| ~ ld__(c,hill) ),
inference(superposition,[status(thm)],[c_49,c_202]) ).
tcf(c_1517,plain,
( sP0(a,b,c)
| sP1(a,b,c)
| sP2(a,b,c)
| sP3(a,b,c)
| sP4(a,b,c)
| ~ ld__(a,k) ),
inference(superposition,[status(thm)],[c_49,c_200]) ).
tcf(c_1536,plain,
( sP0(a,b,c)
| sP1(a,b,c)
| sP2(a,b,c)
| sP3(a,b,c)
| sP4(a,b,c)
| ~ ld__(c,hill) ),
inference(superposition,[status(thm)],[c_49,c_202]) ).
tcf(c_1557,plain,
( sP0(a,b,c)
| sP1(a,b,c)
| sP2(a,b,c)
| sP3(a,b,c)
| sP4(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_1515,c_135,c_390,c_1517]) ).
tcf(c_1569,plain,
( sP0(a,b,c)
| sP1(a,b,c)
| sP2(a,b,c)
| sP3(a,b,c)
| sP4(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_1536,c_135,c_390,c_1517]) ).
tcf(c_1589,plain,
( sP0(g(e,e),w,b)
| sP1(g(e,e),w,b)
| sP2(g(e,e),w,b)
| sP3(g(e,e),w,b)
| sP4(g(e,e),w,b)
| ~ ld__(b,hill) ),
inference(superposition,[status(thm)],[c_50,c_202]) ).
tcf(c_1610,plain,
( sP0(g(e,e),w,b)
| sP1(g(e,e),w,b)
| sP2(g(e,e),w,b)
| sP3(g(e,e),w,b)
| sP4(g(e,e),w,b)
| ~ ld__(b,hill) ),
inference(superposition,[status(thm)],[c_50,c_202]) ).
tcf(c_1631,plain,
( sP0(g(e,e),w,b)
| sP1(g(e,e),w,b)
| sP2(g(e,e),w,b)
| sP3(g(e,e),w,b)
| sP4(g(e,e),w,b) ),
inference(global_subsumption_just,[status(thm)],[c_1589,c_144,c_401,c_1589]) ).
tcf(c_1643,plain,
( sP0(g(e,e),w,b)
| sP1(g(e,e),w,b)
| sP2(g(e,e),w,b)
| sP3(g(e,e),w,b)
| sP4(g(e,e),w,b) ),
inference(global_subsumption_just,[status(thm)],[c_1610,c_1631]) ).
tcf(c_1686,plain,
( sP0(h(d),g(a,c),g(b,b))
| sP1(h(d),g(a,c),g(b,b))
| sP2(h(d),g(a,c),g(b,b))
| sP3(h(d),g(a,c),g(b,b))
| sP4(h(d),g(a,c),g(b,b))
| ~ ld__(h(d),k) ),
inference(superposition,[status(thm)],[c_51,c_200]) ).
tcf(c_1777,plain,
( sP0(h(d),g(e,e),k)
| sP1(h(d),g(e,e),k)
| sP2(h(d),g(e,e),k)
| sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k)
| ~ ld__(k,hill) ),
inference(superposition,[status(thm)],[c_52,c_202]) ).
tcf(c_1798,plain,
( sP0(h(d),g(e,e),k)
| sP1(h(d),g(e,e),k)
| sP2(h(d),g(e,e),k)
| sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k)
| ~ ld__(k,hill) ),
inference(superposition,[status(thm)],[c_52,c_202]) ).
tcf(c_1863,plain,
( sP0(h(d),g(e,e),k)
| sP1(h(d),g(e,e),k)
| sP2(h(d),g(e,e),k)
| sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k) ),
inference(global_subsumption_just,[status(thm)],[c_1777,c_180,c_453,c_1777]) ).
tcf(c_1875,plain,
( sP0(h(d),g(e,e),k)
| sP1(h(d),g(e,e),k)
| sP2(h(d),g(e,e),k)
| sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k) ),
inference(global_subsumption_just,[status(thm)],[c_1798,c_1863]) ).
tcf(c_1901,plain,
( sP0(k,lkg,hill)
| sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(hill,hill) ),
inference(superposition,[status(thm)],[c_53,c_202]) ).
tcf(c_1902,plain,
( sP0(k,lkg,hill)
| sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(lkg,lkg) ),
inference(superposition,[status(thm)],[c_53,c_201]) ).
tcf(c_1922,plain,
( sP0(k,lkg,hill)
| sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(hill,hill) ),
inference(superposition,[status(thm)],[c_53,c_202]) ).
tcf(c_1923,plain,
( sP0(k,lkg,hill)
| sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(lkg,lkg) ),
inference(superposition,[status(thm)],[c_53,c_201]) ).
tcf(c_2066,plain,
( sP0(a,a,a)
| sP1(a,a,a)
| sP2(a,a,a)
| sP3(a,a,a)
| sP4(a,a,a)
| ~ ld__(a,hill) ),
inference(superposition,[status(thm)],[c_54,c_202]) ).
tcf(c_2123,plain,
sP0(a,a,a),
inference(global_subsumption_just,[status(thm)],[c_2066,c_139,c_136,c_135,c_133,c_54,c_244,c_246,c_249,c_251,c_258,c_390,c_391,c_639]) ).
tcf(c_2201,plain,
ld__(b,a),
inference(superposition,[status(thm)],[c_139,c_60]) ).
tcf(c_2203,plain,
ld__(b,w),
inference(superposition,[status(thm)],[c_142,c_60]) ).
tcf(c_2231,plain,
ld__(a,aparna),
inference(superposition,[status(thm)],[c_61,c_60]) ).
tcf(c_2232,plain,
ld__(a,cow),
inference(superposition,[status(thm)],[c_62,c_60]) ).
tcf(c_2233,plain,
ld__(a,horse),
inference(superposition,[status(thm)],[c_63,c_60]) ).
tcf(c_2234,plain,
ld__(a,lilly),
inference(superposition,[status(thm)],[c_64,c_60]) ).
tcf(c_2235,plain,
ld__(a,pig),
inference(superposition,[status(thm)],[c_66,c_60]) ).
tcf(c_2236,plain,
ld__(b,aparna),
inference(superposition,[status(thm)],[c_67,c_60]) ).
tcf(c_2237,plain,
ld__(b,cow),
inference(superposition,[status(thm)],[c_68,c_60]) ).
tcf(c_2238,plain,
ld__(b,horse),
inference(superposition,[status(thm)],[c_69,c_60]) ).
tcf(c_2239,plain,
ld__(b,lilly),
inference(superposition,[status(thm)],[c_70,c_60]) ).
tcf(c_2240,plain,
ld__(b,pig),
inference(superposition,[status(thm)],[c_72,c_60]) ).
tcf(c_2241,plain,
ld__(c,aparna),
inference(superposition,[status(thm)],[c_73,c_60]) ).
tcf(c_2242,plain,
ld__(c,cow),
inference(superposition,[status(thm)],[c_74,c_60]) ).
tcf(c_2243,plain,
ld__(c,horse),
inference(superposition,[status(thm)],[c_75,c_60]) ).
tcf(c_2244,plain,
ld__(c,lilly),
inference(superposition,[status(thm)],[c_76,c_60]) ).
tcf(c_2245,plain,
ld__(c,pig),
inference(superposition,[status(thm)],[c_78,c_60]) ).
tcf(c_2246,plain,
ld__(d,aparna),
inference(superposition,[status(thm)],[c_79,c_60]) ).
tcf(c_2247,plain,
ld__(d,cow),
inference(superposition,[status(thm)],[c_80,c_60]) ).
tcf(c_2248,plain,
ld__(d,horse),
inference(superposition,[status(thm)],[c_81,c_60]) ).
tcf(c_2249,plain,
ld__(d,lilly),
inference(superposition,[status(thm)],[c_82,c_60]) ).
tcf(c_2250,plain,
ld__(d,pig),
inference(superposition,[status(thm)],[c_84,c_60]) ).
tcf(c_2251,plain,
ld__(e,aparna),
inference(superposition,[status(thm)],[c_85,c_60]) ).
tcf(c_2252,plain,
ld__(e,cow),
inference(superposition,[status(thm)],[c_86,c_60]) ).
tcf(c_2253,plain,
ld__(e,horse),
inference(superposition,[status(thm)],[c_87,c_60]) ).
tcf(c_2254,plain,
ld__(e,lilly),
inference(superposition,[status(thm)],[c_88,c_60]) ).
tcf(c_2255,plain,
ld__(e,pig),
inference(superposition,[status(thm)],[c_90,c_60]) ).
tcf(c_2256,plain,
ld__(hill,aparna),
inference(superposition,[status(thm)],[c_103,c_60]) ).
tcf(c_2257,plain,
ld__(hill,cow),
inference(superposition,[status(thm)],[c_104,c_60]) ).
tcf(c_2258,plain,
ld__(hill,horse),
inference(superposition,[status(thm)],[c_105,c_60]) ).
tcf(c_2259,plain,
ld__(hill,lilly),
inference(superposition,[status(thm)],[c_106,c_60]) ).
tcf(c_2260,plain,
ld__(hill,pig),
inference(superposition,[status(thm)],[c_108,c_60]) ).
tcf(c_2261,plain,
ld__(k,aparna),
inference(superposition,[status(thm)],[c_109,c_60]) ).
tcf(c_2262,plain,
ld__(k,cow),
inference(superposition,[status(thm)],[c_110,c_60]) ).
tcf(c_2263,plain,
ld__(k,horse),
inference(superposition,[status(thm)],[c_111,c_60]) ).
tcf(c_2264,plain,
ld__(k,lilly),
inference(superposition,[status(thm)],[c_112,c_60]) ).
tcf(c_2265,plain,
ld__(k,pig),
inference(superposition,[status(thm)],[c_114,c_60]) ).
tcf(c_2266,plain,
ld__(lkg,aparna),
inference(superposition,[status(thm)],[c_115,c_60]) ).
tcf(c_2267,plain,
ld__(lkg,cow),
inference(superposition,[status(thm)],[c_116,c_60]) ).
tcf(c_2268,plain,
ld__(lkg,horse),
inference(superposition,[status(thm)],[c_117,c_60]) ).
tcf(c_2269,plain,
ld__(lkg,lilly),
inference(superposition,[status(thm)],[c_118,c_60]) ).
tcf(c_2270,plain,
ld__(lkg,pig),
inference(superposition,[status(thm)],[c_120,c_60]) ).
tcf(c_2271,plain,
ld__(w,aparna),
inference(superposition,[status(thm)],[c_121,c_60]) ).
tcf(c_2272,plain,
ld__(w,cow),
inference(superposition,[status(thm)],[c_122,c_60]) ).
tcf(c_2273,plain,
ld__(w,horse),
inference(superposition,[status(thm)],[c_123,c_60]) ).
tcf(c_2274,plain,
ld__(w,lilly),
inference(superposition,[status(thm)],[c_124,c_60]) ).
tcf(c_2275,plain,
ld__(w,pig),
inference(superposition,[status(thm)],[c_126,c_60]) ).
tcf(c_2276,plain,
ld__(a,w),
inference(superposition,[status(thm)],[c_130,c_60]) ).
tcf(c_2277,plain,
ld__(a,d),
inference(superposition,[status(thm)],[c_131,c_60]) ).
tcf(c_2278,plain,
ld__(a,lkg),
inference(superposition,[status(thm)],[c_132,c_60]) ).
tcf(c_2279,plain,
ld__(c,a),
inference(superposition,[status(thm)],[c_133,c_60]) ).
tcf(c_2280,plain,
ld__(a,k),
inference(superposition,[status(thm)],[c_135,c_60]) ).
tcf(c_2281,plain,
ld__(a,hill),
inference(superposition,[status(thm)],[c_136,c_60]) ).
tcf(c_2282,plain,
ld__(a,e),
inference(superposition,[status(thm)],[c_137,c_60]) ).
tcf(c_2283,plain,
ld__(b,a),
inference(superposition,[status(thm)],[c_139,c_60]) ).
tcf(c_2284,plain,
ld__(b,k),
inference(superposition,[status(thm)],[c_141,c_60]) ).
tcf(c_2285,plain,
ld__(b,w),
inference(superposition,[status(thm)],[c_142,c_60]) ).
tcf(c_2286,plain,
ld__(b,d),
inference(superposition,[status(thm)],[c_143,c_60]) ).
tcf(c_2287,plain,
ld__(b,hill),
inference(superposition,[status(thm)],[c_144,c_60]) ).
tcf(c_2288,plain,
ld__(b,e),
inference(superposition,[status(thm)],[c_146,c_60]) ).
tcf(c_2289,plain,
ld__(c,b),
inference(superposition,[status(thm)],[c_147,c_60]) ).
tcf(c_2290,plain,
ld__(b,lkg),
inference(superposition,[status(thm)],[c_148,c_60]) ).
tcf(c_2291,plain,
ld__(c,w),
inference(superposition,[status(thm)],[c_149,c_60]) ).
tcf(c_2292,plain,
ld__(c,lkg),
inference(superposition,[status(thm)],[c_151,c_60]) ).
tcf(c_2293,plain,
ld__(c,e),
inference(superposition,[status(thm)],[c_152,c_60]) ).
tcf(c_2294,plain,
ld__(c,d),
inference(superposition,[status(thm)],[c_153,c_60]) ).
tcf(c_2295,plain,
ld__(c,k),
inference(superposition,[status(thm)],[c_154,c_60]) ).
tcf(c_2296,plain,
ld__(c,hill),
inference(superposition,[status(thm)],[c_156,c_60]) ).
tcf(c_2297,plain,
ld__(d,lkg),
inference(superposition,[status(thm)],[c_157,c_60]) ).
tcf(c_2298,plain,
ld__(d,k),
inference(superposition,[status(thm)],[c_159,c_60]) ).
tcf(c_2299,plain,
ld__(d,hill),
inference(superposition,[status(thm)],[c_160,c_60]) ).
tcf(c_2300,plain,
ld__(w,d),
inference(superposition,[status(thm)],[c_161,c_60]) ).
tcf(c_2301,plain,
ld__(e,d),
inference(superposition,[status(thm)],[c_163,c_60]) ).
tcf(c_2302,plain,
ld__(w,e),
inference(superposition,[status(thm)],[c_165,c_60]) ).
tcf(c_2303,plain,
ld__(e,lkg),
inference(superposition,[status(thm)],[c_167,c_60]) ).
tcf(c_2304,plain,
ld__(e,hill),
inference(superposition,[status(thm)],[c_168,c_60]) ).
tcf(c_2305,plain,
ld__(e,k),
inference(superposition,[status(thm)],[c_169,c_60]) ).
tcf(c_2306,plain,
ld__(hill,lkg),
inference(superposition,[status(thm)],[c_179,c_60]) ).
tcf(c_2307,plain,
ld__(k,hill),
inference(superposition,[status(thm)],[c_180,c_60]) ).
tcf(c_2308,plain,
ld__(w,hill),
inference(superposition,[status(thm)],[c_181,c_60]) ).
tcf(c_3020,plain,
ld__(w,k),
inference(superposition,[status(thm)],[c_182,c_60]) ).
tcf(c_3028,plain,
ld__(k,lkg),
inference(superposition,[status(thm)],[c_183,c_60]) ).
tcf(c_3042,plain,
ld__(w,lkg),
inference(superposition,[status(thm)],[c_184,c_60]) ).
tcf(c_3051,plain,
! [X0: $i] : ld__(pet(X0),a),
inference(superposition,[status(thm)],[c_65,c_60]) ).
tcf(c_3086,plain,
! [X0: $i] : ld__(pet(X0),b),
inference(superposition,[status(thm)],[c_71,c_60]) ).
tcf(c_3095,plain,
! [X0: $i] : ld__(pet(X0),c),
inference(superposition,[status(thm)],[c_77,c_60]) ).
tcf(c_3118,plain,
! [X0: $i] : ld__(pet(X0),d),
inference(superposition,[status(thm)],[c_83,c_60]) ).
tcf(c_3127,plain,
! [X0: $i] : ld__(pet(X0),e),
inference(superposition,[status(thm)],[c_89,c_60]) ).
tcf(c_3162,plain,
! [X0: $i] : ld__(h(X0),aparna),
inference(superposition,[status(thm)],[c_97,c_60]) ).
tcf(c_3171,plain,
! [X0: $i] : ld__(h(X0),cow),
inference(superposition,[status(thm)],[c_98,c_60]) ).
tcf(c_3186,plain,
! [X0: $i] : ld__(h(X0),horse),
inference(superposition,[status(thm)],[c_99,c_60]) ).
tcf(c_3195,plain,
! [X0: $i] : ld__(h(X0),lilly),
inference(superposition,[status(thm)],[c_100,c_60]) ).
tcf(c_3230,plain,
! [X0: $i] : ld__(h(X0),pig),
inference(superposition,[status(thm)],[c_102,c_60]) ).
tcf(c_3239,plain,
! [X0: $i] : ld__(pet(X0),hill),
inference(superposition,[status(thm)],[c_107,c_60]) ).
tcf(c_3254,plain,
! [X0: $i] : ld__(pet(X0),k),
inference(superposition,[status(thm)],[c_113,c_60]) ).
tcf(c_3263,plain,
! [X0: $i] : ld__(pet(X0),lkg),
inference(superposition,[status(thm)],[c_119,c_60]) ).
tcf(c_3298,plain,
! [X0: $i] : ld__(pet(X0),w),
inference(superposition,[status(thm)],[c_125,c_60]) ).
tcf(c_3305,plain,
! [X0: $i] : ld__(h(X0),a),
inference(superposition,[status(thm)],[c_134,c_60]) ).
tcf(c_3307,plain,
! [X0: $i] : ld__(h(X0),a),
inference(superposition,[status(thm)],[c_134,c_60]) ).
tcf(c_3322,plain,
! [X0: $i] : ld__(h(X0),b),
inference(superposition,[status(thm)],[c_145,c_60]) ).
tcf(c_3331,plain,
! [X0: $i] : ld__(h(X0),c),
inference(superposition,[status(thm)],[c_155,c_60]) ).
tcf(c_3366,plain,
! [X0: $i] : ld__(h(X0),d),
inference(superposition,[status(thm)],[c_162,c_60]) ).
tcf(c_3375,plain,
! [X0: $i] : ld__(h(X0),e),
inference(superposition,[status(thm)],[c_164,c_60]) ).
tcf(c_3390,plain,
! [X0: $i] : ld__(h(X0),lkg),
inference(superposition,[status(thm)],[c_175,c_60]) ).
tcf(c_3399,plain,
! [X0: $i] : ld__(h(X0),hill),
inference(superposition,[status(thm)],[c_176,c_60]) ).
tcf(c_3434,plain,
! [X0: $i] : ld__(h(X0),w),
inference(superposition,[status(thm)],[c_177,c_60]) ).
tcf(c_3449,plain,
! [X0: $i] : ld__(h(X0),k),
inference(superposition,[status(thm)],[c_178,c_60]) ).
tcf(c_3450,plain,
( sP0(h(d),g(a,c),g(b,b))
| sP1(h(d),g(a,c),g(b,b))
| sP2(h(d),g(a,c),g(b,b))
| sP3(h(d),g(a,c),g(b,b))
| sP4(h(d),g(a,c),g(b,b)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1686,c_3449]) ).
tcf(c_3478,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),aparna),
inference(superposition,[status(thm)],[c_91,c_60]) ).
tcf(c_3692,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),cow),
inference(superposition,[status(thm)],[c_92,c_60]) ).
tcf(c_3746,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),horse),
inference(superposition,[status(thm)],[c_93,c_60]) ).
tcf(c_3749,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),lilly),
inference(superposition,[status(thm)],[c_94,c_60]) ).
tcf(c_3752,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),pig),
inference(superposition,[status(thm)],[c_96,c_60]) ).
tcf(c_3762,plain,
! [X0: $i,X1: $i] : ld__(h(X0),pet(X1)),
inference(superposition,[status(thm)],[c_101,c_60]) ).
tcf(c_3803,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),a),
inference(superposition,[status(thm)],[c_138,c_60]) ).
tcf(c_3805,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),a),
inference(superposition,[status(thm)],[c_138,c_60]) ).
tcf(c_3815,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),b),
inference(superposition,[status(thm)],[c_140,c_60]) ).
tcf(c_3832,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),c),
inference(superposition,[status(thm)],[c_150,c_60]) ).
tcf(c_3849,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),d),
inference(superposition,[status(thm)],[c_158,c_60]) ).
tcf(c_3868,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),e),
inference(superposition,[status(thm)],[c_166,c_60]) ).
tcf(c_3878,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),w),
inference(superposition,[status(thm)],[c_171,c_60]) ).
tcf(c_3903,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),k),
inference(superposition,[status(thm)],[c_172,c_60]) ).
tcf(c_3906,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),lkg),
inference(superposition,[status(thm)],[c_173,c_60]) ).
tcf(c_3923,plain,
! [X0: $i,X1: $i] : ld__(g(X0,X1),hill),
inference(superposition,[status(thm)],[c_174,c_60]) ).
tcf(c_3954,plain,
! [X0: $i,X1: $i,X2: $i] : ld__(g(X0,X1),pet(X2)),
inference(superposition,[status(thm)],[c_95,c_60]) ).
tcf(c_3962,plain,
! [X0: $i,X1: $i,X2: $i] : ld__(g(X0,X1),h(X2)),
inference(superposition,[status(thm)],[c_170,c_60]) ).
tcf(c_3964,plain,
! [X0: $i,X1: $i,X2: $i] : ld__(g(X0,X1),h(X2)),
inference(superposition,[status(thm)],[c_170,c_60]) ).
tcf(c_3990,plain,
! [X0: $i,X1: $i] :
( ld__(h(X1),h(X0))
| ~ ld__(X0,X1) ),
inference(superposition,[status(thm)],[c_129,c_60]) ).
tcf(c_4360,plain,
! [X0: $i,X1: $i] : ~ sP1(a,X0,X1),
inference(superposition,[status(thm)],[c_134,c_194]) ).
tcf(c_4368,plain,
! [X0: $i,X1: $i] : ~ sP1(k,X0,X1),
inference(superposition,[status(thm)],[c_178,c_194]) ).
tcf(c_4369,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ~ sP1(g(X0,X1),X2,X3),
inference(superposition,[status(thm)],[c_3962,c_194]) ).
tcf(c_4419,plain,
! [X0: $i,X1: $i] : ~ sP1(aparna,X0,X1),
inference(superposition,[status(thm)],[c_97,c_194]) ).
tcf(c_4420,plain,
! [X0: $i,X1: $i] : ~ sP1(cow,X0,X1),
inference(superposition,[status(thm)],[c_98,c_194]) ).
tcf(c_4421,plain,
! [X0: $i,X1: $i] : ~ sP1(horse,X0,X1),
inference(superposition,[status(thm)],[c_99,c_194]) ).
tcf(c_4422,plain,
! [X0: $i,X1: $i] : ~ sP1(lilly,X0,X1),
inference(superposition,[status(thm)],[c_100,c_194]) ).
tcf(c_4423,plain,
! [X0: $i,X1: $i,X2: $i] : ~ sP1(pet(X0),X1,X2),
inference(superposition,[status(thm)],[c_101,c_194]) ).
tcf(c_4424,plain,
! [X0: $i,X1: $i] : ~ sP1(pig,X0,X1),
inference(superposition,[status(thm)],[c_102,c_194]) ).
tcf(c_4425,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(d,X0)
| ~ sP1(h(X0),X1,X2) ),
inference(superposition,[status(thm)],[c_3990,c_194]) ).
tcf(c_4426,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X0,d)
| ~ sP1(h(X0),X1,X2) ),
inference(superposition,[status(thm)],[c_129,c_194]) ).
tcf(c_4427,plain,
! [X0: $i,X1: $i] : ~ sP1(a,X0,X1),
inference(superposition,[status(thm)],[c_134,c_194]) ).
tcf(c_4428,plain,
! [X0: $i,X1: $i] : ~ sP1(b,X0,X1),
inference(superposition,[status(thm)],[c_145,c_194]) ).
tcf(c_4429,plain,
! [X0: $i,X1: $i] : ~ sP1(c,X0,X1),
inference(superposition,[status(thm)],[c_155,c_194]) ).
tcf(c_4430,plain,
! [X0: $i,X1: $i] : ~ sP1(d,X0,X1),
inference(superposition,[status(thm)],[c_162,c_194]) ).
tcf(c_4431,plain,
! [X0: $i,X1: $i] : ~ sP1(e,X0,X1),
inference(superposition,[status(thm)],[c_164,c_194]) ).
tcf(c_4432,plain,
! [X0: $i,X1: $i] : ~ sP1(lkg,X0,X1),
inference(superposition,[status(thm)],[c_175,c_194]) ).
tcf(c_4433,plain,
! [X0: $i,X1: $i] : ~ sP1(hill,X0,X1),
inference(superposition,[status(thm)],[c_176,c_194]) ).
tcf(c_4434,plain,
! [X0: $i,X1: $i] : ~ sP1(w,X0,X1),
inference(superposition,[status(thm)],[c_177,c_194]) ).
tcf(c_4435,plain,
! [X0: $i,X1: $i] : ~ sP1(k,X0,X1),
inference(superposition,[status(thm)],[c_178,c_194]) ).
tcf(c_4436,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ~ sP1(g(X0,X1),X2,X3),
inference(superposition,[status(thm)],[c_3964,c_194]) ).
tcf(c_4702,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ld__(g(X1,X2),g(X0,X3))
| ~ ld__(X0,X1) ),
inference(superposition,[status(thm)],[c_127,c_60]) ).
tcf(c_4727,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ld__(g(X2,X1),g(X3,X0))
| ~ ld__(X0,X1) ),
inference(superposition,[status(thm)],[c_128,c_60]) ).
tcf(c_4788,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,aparna,X1),
inference(superposition,[status(thm)],[c_91,c_186]) ).
tcf(c_4789,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,cow,X1),
inference(superposition,[status(thm)],[c_92,c_186]) ).
tcf(c_4790,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,horse,X1),
inference(superposition,[status(thm)],[c_93,c_186]) ).
tcf(c_4791,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,lilly,X1),
inference(superposition,[status(thm)],[c_94,c_186]) ).
tcf(c_4792,plain,
! [X0: $i,X1: $i,X2: $i] : ~ sP4(X0,pet(X1),X2),
inference(superposition,[status(thm)],[c_95,c_186]) ).
tcf(c_4793,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,pig,X1),
inference(superposition,[status(thm)],[c_96,c_186]) ).
tcf(c_4794,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(X1,e)
| ~ sP4(X0,g(X1,X2),X3) ),
inference(superposition,[status(thm)],[c_127,c_186]) ).
tcf(c_4795,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(X2,e)
| ~ sP4(X0,g(X1,X2),X3) ),
inference(superposition,[status(thm)],[c_128,c_186]) ).
tcf(c_4796,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,a,X1),
inference(superposition,[status(thm)],[c_138,c_186]) ).
tcf(c_4797,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,b,X1),
inference(superposition,[status(thm)],[c_140,c_186]) ).
tcf(c_4798,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,c,X1),
inference(superposition,[status(thm)],[c_150,c_186]) ).
tcf(c_4799,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,d,X1),
inference(superposition,[status(thm)],[c_158,c_186]) ).
tcf(c_4800,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,e,X1),
inference(superposition,[status(thm)],[c_166,c_186]) ).
tcf(c_4801,plain,
! [X0: $i,X1: $i,X2: $i] : ~ sP4(X0,h(X1),X2),
inference(superposition,[status(thm)],[c_170,c_186]) ).
tcf(c_4802,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,w,X1),
inference(superposition,[status(thm)],[c_171,c_186]) ).
tcf(c_4803,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,k,X1),
inference(superposition,[status(thm)],[c_172,c_186]) ).
tcf(c_4804,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,lkg,X1),
inference(superposition,[status(thm)],[c_173,c_186]) ).
tcf(c_4805,plain,
! [X0: $i,X1: $i] : ~ sP4(X0,hill,X1),
inference(superposition,[status(thm)],[c_174,c_186]) ).
tcf(c_5018,plain,
! [X0: $i,X1: $i,X2: $i] : ~ sP2(h(X0),X1,X2),
inference(superposition,[status(thm)],[c_170,c_191]) ).
tcf(c_5056,plain,
! [X0: $i,X1: $i] : ~ sP2(aparna,X0,X1),
inference(superposition,[status(thm)],[c_91,c_191]) ).
tcf(c_5057,plain,
! [X0: $i,X1: $i] : ~ sP2(cow,X0,X1),
inference(superposition,[status(thm)],[c_92,c_191]) ).
tcf(c_5058,plain,
! [X0: $i,X1: $i] : ~ sP2(horse,X0,X1),
inference(superposition,[status(thm)],[c_93,c_191]) ).
tcf(c_5059,plain,
! [X0: $i,X1: $i] : ~ sP2(lilly,X0,X1),
inference(superposition,[status(thm)],[c_94,c_191]) ).
tcf(c_5060,plain,
! [X0: $i,X1: $i,X2: $i] : ~ sP2(pet(X0),X1,X2),
inference(superposition,[status(thm)],[c_95,c_191]) ).
tcf(c_5061,plain,
! [X0: $i,X1: $i] : ~ sP2(pig,X0,X1),
inference(superposition,[status(thm)],[c_96,c_191]) ).
tcf(c_5062,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(X0,e)
| ~ sP2(g(X0,X1),X2,X3) ),
inference(superposition,[status(thm)],[c_127,c_191]) ).
tcf(c_5063,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(X1,e)
| ~ sP2(g(X0,X1),X2,X3) ),
inference(superposition,[status(thm)],[c_128,c_191]) ).
tcf(c_5064,plain,
! [X0: $i,X1: $i] : ~ sP2(a,X0,X1),
inference(superposition,[status(thm)],[c_138,c_191]) ).
tcf(c_5065,plain,
! [X0: $i,X1: $i] : ~ sP2(b,X0,X1),
inference(superposition,[status(thm)],[c_140,c_191]) ).
tcf(c_5066,plain,
! [X0: $i,X1: $i] : ~ sP2(c,X0,X1),
inference(superposition,[status(thm)],[c_150,c_191]) ).
tcf(c_5067,plain,
! [X0: $i,X1: $i] : ~ sP2(d,X0,X1),
inference(superposition,[status(thm)],[c_158,c_191]) ).
tcf(c_5068,plain,
! [X0: $i,X1: $i] : ~ sP2(e,X0,X1),
inference(superposition,[status(thm)],[c_166,c_191]) ).
tcf(c_5069,plain,
! [X0: $i,X1: $i,X2: $i] : ~ sP2(h(X0),X1,X2),
inference(superposition,[status(thm)],[c_170,c_191]) ).
tcf(c_5070,plain,
! [X0: $i,X1: $i] : ~ sP2(w,X0,X1),
inference(superposition,[status(thm)],[c_171,c_191]) ).
tcf(c_5071,plain,
! [X0: $i,X1: $i] : ~ sP2(k,X0,X1),
inference(superposition,[status(thm)],[c_172,c_191]) ).
tcf(c_5072,plain,
! [X0: $i,X1: $i] : ~ sP2(lkg,X0,X1),
inference(superposition,[status(thm)],[c_173,c_191]) ).
tcf(c_5073,plain,
! [X0: $i,X1: $i] : ~ sP2(hill,X0,X1),
inference(superposition,[status(thm)],[c_174,c_191]) ).
tcf(c_5593,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,aparna,X1),
inference(superposition,[status(thm)],[c_91,c_195]) ).
tcf(c_5594,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,cow,X1),
inference(superposition,[status(thm)],[c_92,c_195]) ).
tcf(c_5595,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,horse,X1),
inference(superposition,[status(thm)],[c_93,c_195]) ).
tcf(c_5596,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,lilly,X1),
inference(superposition,[status(thm)],[c_94,c_195]) ).
tcf(c_5597,plain,
! [X0: $i,X1: $i,X2: $i] : ~ sP1(X0,pet(X1),X2),
inference(superposition,[status(thm)],[c_95,c_195]) ).
tcf(c_5598,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,pig,X1),
inference(superposition,[status(thm)],[c_96,c_195]) ).
tcf(c_5599,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(X1,a)
| ~ sP1(X0,g(X1,X2),X3) ),
inference(superposition,[status(thm)],[c_127,c_195]) ).
tcf(c_5600,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(X2,c)
| ~ sP1(X0,g(X1,X2),X3) ),
inference(superposition,[status(thm)],[c_128,c_195]) ).
tcf(c_5601,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,a,X1),
inference(superposition,[status(thm)],[c_138,c_195]) ).
tcf(c_5602,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,b,X1),
inference(superposition,[status(thm)],[c_140,c_195]) ).
tcf(c_5603,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,c,X1),
inference(superposition,[status(thm)],[c_150,c_195]) ).
tcf(c_5604,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,d,X1),
inference(superposition,[status(thm)],[c_158,c_195]) ).
tcf(c_5605,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,e,X1),
inference(superposition,[status(thm)],[c_166,c_195]) ).
tcf(c_5606,plain,
! [X0: $i,X1: $i,X2: $i] : ~ sP1(X0,h(X1),X2),
inference(superposition,[status(thm)],[c_170,c_195]) ).
tcf(c_5607,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,w,X1),
inference(superposition,[status(thm)],[c_171,c_195]) ).
tcf(c_5608,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,k,X1),
inference(superposition,[status(thm)],[c_172,c_195]) ).
tcf(c_5609,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,lkg,X1),
inference(superposition,[status(thm)],[c_173,c_195]) ).
tcf(c_5610,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,hill,X1),
inference(superposition,[status(thm)],[c_174,c_195]) ).
tcf(c_5736,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,k),
inference(superposition,[status(thm)],[c_172,c_196]) ).
tcf(c_5808,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,aparna),
inference(superposition,[status(thm)],[c_91,c_196]) ).
tcf(c_5809,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,cow),
inference(superposition,[status(thm)],[c_92,c_196]) ).
tcf(c_5810,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,horse),
inference(superposition,[status(thm)],[c_93,c_196]) ).
tcf(c_5811,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,lilly),
inference(superposition,[status(thm)],[c_94,c_196]) ).
tcf(c_5812,plain,
! [X0: $i,X1: $i,X2: $i] : ~ sP1(X0,X1,pet(X2)),
inference(superposition,[status(thm)],[c_95,c_196]) ).
tcf(c_5813,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,pig),
inference(superposition,[status(thm)],[c_96,c_196]) ).
tcf(c_5814,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(X2,b)
| ~ sP1(X0,X1,g(X2,X3)) ),
inference(superposition,[status(thm)],[c_127,c_196]) ).
tcf(c_5815,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(X3,b)
| ~ sP1(X0,X1,g(X2,X3)) ),
inference(superposition,[status(thm)],[c_128,c_196]) ).
tcf(c_5816,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,a),
inference(superposition,[status(thm)],[c_138,c_196]) ).
tcf(c_5817,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,b),
inference(superposition,[status(thm)],[c_140,c_196]) ).
tcf(c_5818,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,c),
inference(superposition,[status(thm)],[c_150,c_196]) ).
tcf(c_5819,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,d),
inference(superposition,[status(thm)],[c_158,c_196]) ).
tcf(c_5820,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,e),
inference(superposition,[status(thm)],[c_166,c_196]) ).
tcf(c_5821,plain,
! [X0: $i,X1: $i,X2: $i] : ~ sP1(X0,X1,h(X2)),
inference(superposition,[status(thm)],[c_170,c_196]) ).
tcf(c_5822,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,w),
inference(superposition,[status(thm)],[c_171,c_196]) ).
tcf(c_5823,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,k),
inference(superposition,[status(thm)],[c_172,c_196]) ).
tcf(c_5824,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,lkg),
inference(superposition,[status(thm)],[c_173,c_196]) ).
tcf(c_5825,plain,
! [X0: $i,X1: $i] : ~ sP1(X0,X1,hill),
inference(superposition,[status(thm)],[c_174,c_196]) ).
tcf(c_6075,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(e,X0)
| ~ sP2(g(X0,X1),X2,X3) ),
inference(superposition,[status(thm)],[c_4702,c_191]) ).
tcf(c_6076,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(e,X1)
| ~ sP4(X0,g(X1,X2),X3) ),
inference(superposition,[status(thm)],[c_4702,c_186]) ).
tcf(c_6077,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(a,X1)
| ~ sP1(X0,g(X1,X2),X3) ),
inference(superposition,[status(thm)],[c_4702,c_195]) ).
tcf(c_6078,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(b,X2)
| ~ sP1(X0,X1,g(X2,X3)) ),
inference(superposition,[status(thm)],[c_4702,c_196]) ).
tcf(c_6131,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(e,X1)
| ~ sP2(g(X0,X1),X2,X3) ),
inference(superposition,[status(thm)],[c_4727,c_191]) ).
tcf(c_6132,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(e,X2)
| ~ sP4(X0,g(X1,X2),X3) ),
inference(superposition,[status(thm)],[c_4727,c_186]) ).
tcf(c_6133,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(c,X2)
| ~ sP1(X0,g(X1,X2),X3) ),
inference(superposition,[status(thm)],[c_4727,c_195]) ).
tcf(c_6134,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ld__(b,X3)
| ~ sP1(X0,X1,g(X2,X3)) ),
inference(superposition,[status(thm)],[c_4727,c_196]) ).
fof(f142,definition,
! [X0,X1,X2] :
( ~ sP0(X0,X1,X2)
| ( ~ ld__(X2,a)
& ~ ld__(X1,a)
& ~ ld__(X0,a) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f143,definition,
! [X0,X1,X2] :
( ~ sP1(X0,X1,X2)
| ( ~ ld__(X2,g(b,b))
& ~ ld__(X1,g(a,c))
& ~ ld__(X0,h(d)) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f144,definition,
! [X0,X1,X2] :
( ~ sP2(X0,X1,X2)
| ( ~ ld__(X2,b)
& ~ ld__(X1,w)
& ~ ld__(X0,g(e,e)) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f145,definition,
! [X0,X1,X2] :
( ~ sP3(X0,X1,X2)
| ( ~ ld__(X2,c)
& ~ ld__(X1,b)
& ~ ld__(X0,a) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f146,definition,
! [X0,X1,X2] :
( ~ sP4(X0,X1,X2)
| ( ~ ld__(X2,k)
& ~ ld__(X1,g(e,e))
& ~ ld__(X0,h(d)) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f147,plain,
! [X0,X1,X2] :
( sP0(X0,X1,X2)
| sP1(X0,X1,X2)
| sP2(X0,X1,X2)
| sP3(X0,X1,X2)
| sP4(X0,X1,X2)
| ( ~ ld__(X2,hill)
& ~ ld__(X1,lkg)
& ~ ld__(X0,k) )
| ~ p(X0,X1,X2) ),
inference(definition_folding,[],[f141,f146,f145,f144,f143,f142]) ).
fof(f152,plain,
! [X0,X1,X2] :
( ~ sP0(X0,X1,X2)
| ( ~ ld__(X2,a)
& ~ ld__(X1,a)
& ~ ld__(X0,a) ) ),
inference(nnf_transformation,[],[f142]) ).
fof(f301,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| ~ ld__(X2,a) ),
inference(cnf_transformation,[],[f152]) ).
fof(f302,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| ~ ld__(X1,a) ),
inference(cnf_transformation,[],[f152]) ).
fof(f303,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| ~ ld__(X0,a) ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_197,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X0,a)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f303]) ).
tcf(c_198,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X1,a)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f302]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ld__(X2,a)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f301]) ).
tcf(c_4092,plain,
( sP1(g(e,e),w,b)
| sP2(g(e,e),w,b)
| sP3(g(e,e),w,b)
| sP4(g(e,e),w,b)
| ~ ld__(g(e,e),a) ),
inference(superposition,[status(thm)],[c_1631,c_197]) ).
tcf(c_4094,plain,
( sP1(h(d),g(e,e),k)
| sP2(h(d),g(e,e),k)
| sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k)
| ~ ld__(h(d),a) ),
inference(superposition,[status(thm)],[c_1863,c_197]) ).
tcf(c_4096,plain,
( sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(lkg,lkg)
| ~ ld__(k,a) ),
inference(superposition,[status(thm)],[c_1902,c_197]) ).
tcf(c_4097,plain,
( sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(hill,hill)
| ~ ld__(k,a) ),
inference(superposition,[status(thm)],[c_1901,c_197]) ).
tcf(c_4098,plain,
( sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(hill,hill) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4097,c_135]) ).
tcf(c_4104,plain,
( sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(lkg,lkg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4096,c_135]) ).
tcf(c_4116,plain,
( sP1(g(e,e),w,b)
| sP2(g(e,e),w,b)
| sP3(g(e,e),w,b)
| sP4(g(e,e),w,b) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4092,c_3803]) ).
tcf(c_4121,plain,
( sP1(h(d),g(e,e),k)
| sP2(h(d),g(e,e),k)
| sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4094,c_3305]) ).
tcf(c_4135,plain,
~ ld__(a,a),
inference(superposition,[status(thm)],[c_2123,c_197]) ).
tcf(c_4137,plain,
( sP1(g(e,e),w,b)
| sP2(g(e,e),w,b)
| sP3(g(e,e),w,b)
| sP4(g(e,e),w,b)
| ~ ld__(g(e,e),a) ),
inference(superposition,[status(thm)],[c_1643,c_197]) ).
tcf(c_4138,plain,
( sP1(h(d),g(a,c),g(b,b))
| sP2(h(d),g(a,c),g(b,b))
| sP3(h(d),g(a,c),g(b,b))
| sP4(h(d),g(a,c),g(b,b))
| ~ ld__(h(d),a) ),
inference(superposition,[status(thm)],[c_3450,c_197]) ).
tcf(c_4139,plain,
( sP1(h(d),g(e,e),k)
| sP2(h(d),g(e,e),k)
| sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k)
| ~ ld__(h(d),a) ),
inference(superposition,[status(thm)],[c_1875,c_197]) ).
tcf(c_4141,plain,
( sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(lkg,lkg)
| ~ ld__(k,a) ),
inference(superposition,[status(thm)],[c_1923,c_197]) ).
tcf(c_4142,plain,
( sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(hill,hill)
| ~ ld__(k,a) ),
inference(superposition,[status(thm)],[c_1922,c_197]) ).
tcf(c_4143,plain,
( sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(hill,hill) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4142,c_135]) ).
tcf(c_4149,plain,
( sP1(k,lkg,hill)
| sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(lkg,lkg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4141,c_135]) ).
tcf(c_4161,plain,
( sP1(g(e,e),w,b)
| sP2(g(e,e),w,b)
| sP3(g(e,e),w,b)
| sP4(g(e,e),w,b) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4137,c_3805]) ).
tcf(c_4166,plain,
( sP1(h(d),g(e,e),k)
| sP2(h(d),g(e,e),k)
| sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4139,c_3307]) ).
tcf(c_4171,plain,
( sP1(h(d),g(a,c),g(b,b))
| sP2(h(d),g(a,c),g(b,b))
| sP3(h(d),g(a,c),g(b,b))
| sP4(h(d),g(a,c),g(b,b)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4138,c_3307]) ).
tcf(c_4189,plain,
( sP1(a,b,c)
| sP2(a,b,c)
| sP3(a,b,c)
| sP4(a,b,c)
| ~ ld__(b,a) ),
inference(superposition,[status(thm)],[c_1557,c_198]) ).
tcf(c_4190,plain,
( sP1(a,b,c)
| sP2(a,b,c)
| sP3(a,b,c)
| sP4(a,b,c) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4189,c_2201]) ).
tcf(c_4200,plain,
( sP1(a,b,c)
| sP2(a,b,c)
| sP3(a,b,c)
| sP4(a,b,c)
| ~ ld__(b,a) ),
inference(superposition,[status(thm)],[c_1569,c_198]) ).
tcf(c_4201,plain,
( sP1(a,b,c)
| sP2(a,b,c)
| sP3(a,b,c)
| sP4(a,b,c) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4200,c_2283]) ).
tcf(c_4374,plain,
( sP2(a,b,c)
| sP3(a,b,c)
| sP4(a,b,c) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4190,c_4360]) ).
tcf(c_4379,plain,
( sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(lkg,lkg) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4104,c_4368]) ).
tcf(c_4380,plain,
( sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(hill,hill) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4098,c_4368]) ).
tcf(c_4393,plain,
( sP2(g(e,e),w,b)
| sP3(g(e,e),w,b)
| sP4(g(e,e),w,b) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4116,c_4369]) ).
tcf(c_4441,plain,
( sP2(a,b,c)
| sP3(a,b,c)
| sP4(a,b,c) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4201,c_4427]) ).
tcf(c_4446,plain,
( sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(lkg,lkg) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4149,c_4435]) ).
tcf(c_4447,plain,
( sP2(k,lkg,hill)
| sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(hill,hill) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4143,c_4435]) ).
tcf(c_4460,plain,
( sP2(g(e,e),w,b)
| sP3(g(e,e),w,b)
| sP4(g(e,e),w,b) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4161,c_4436]) ).
tcf(c_5028,plain,
( sP1(h(d),g(e,e),k)
| sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4121,c_5018]) ).
tcf(c_5078,plain,
( sP1(h(d),g(a,c),g(b,b))
| sP3(h(d),g(a,c),g(b,b))
| sP4(h(d),g(a,c),g(b,b)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4171,c_5069]) ).
tcf(c_5079,plain,
( sP1(h(d),g(e,e),k)
| sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4166,c_5069]) ).
tcf(c_5283,plain,
( sP3(a,b,c)
| sP4(a,b,c)
| ~ ld__(b,w) ),
inference(superposition,[status(thm)],[c_4374,c_192]) ).
tcf(c_5284,plain,
( sP3(a,b,c)
| sP4(a,b,c) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5283,c_2203]) ).
tcf(c_5287,plain,
( sP4(a,b,c)
| sP3(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_4441,c_5284]) ).
tcf(c_5288,plain,
( sP3(a,b,c)
| sP4(a,b,c) ),
inference(renaming,[status(thm)],[c_5287]) ).
tcf(c_5293,plain,
( sP4(a,b,c)
| ~ ld__(c,c) ),
inference(superposition,[status(thm)],[c_5288,c_190]) ).
tcf(c_5294,plain,
( sP4(a,b,c)
| ~ ld__(b,b) ),
inference(superposition,[status(thm)],[c_5288,c_189]) ).
tcf(c_5331,plain,
( sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(lkg,lkg)
| ~ ld__(lkg,w) ),
inference(superposition,[status(thm)],[c_4379,c_192]) ).
tcf(c_5332,plain,
( sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(lkg,lkg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5331,c_184]) ).
tcf(c_5345,plain,
( sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(hill,hill)
| ~ ld__(lkg,w) ),
inference(superposition,[status(thm)],[c_4380,c_192]) ).
tcf(c_5346,plain,
( sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(hill,hill) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5345,c_184]) ).
tcf(c_5357,plain,
( sP3(g(e,e),w,b)
| sP4(g(e,e),w,b)
| ~ ld__(w,w) ),
inference(superposition,[status(thm)],[c_4393,c_192]) ).
tcf(c_5408,plain,
( ~ ld__(lkg,lkg)
| sP4(k,lkg,hill)
| sP3(k,lkg,hill) ),
inference(global_subsumption_just,[status(thm)],[c_4446,c_5332]) ).
tcf(c_5409,plain,
( sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(lkg,lkg) ),
inference(renaming,[status(thm)],[c_5408]) ).
tcf(c_5418,plain,
( sP4(k,lkg,hill)
| ~ ld__(lkg,lkg)
| ~ ld__(k,a) ),
inference(superposition,[status(thm)],[c_5409,c_188]) ).
tcf(c_5419,plain,
( sP4(k,lkg,hill)
| ~ ld__(lkg,lkg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5418,c_135]) ).
tcf(c_5427,plain,
( ~ ld__(hill,hill)
| sP4(k,lkg,hill)
| sP3(k,lkg,hill) ),
inference(global_subsumption_just,[status(thm)],[c_4447,c_5346]) ).
tcf(c_5428,plain,
( sP3(k,lkg,hill)
| sP4(k,lkg,hill)
| ~ ld__(hill,hill) ),
inference(renaming,[status(thm)],[c_5427]) ).
tcf(c_5437,plain,
( sP4(k,lkg,hill)
| ~ ld__(hill,hill)
| ~ ld__(k,a) ),
inference(superposition,[status(thm)],[c_5428,c_188]) ).
tcf(c_5438,plain,
( sP4(k,lkg,hill)
| ~ ld__(hill,hill) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5437,c_135]) ).
tcf(c_5490,plain,
( sP3(g(e,e),w,b)
| sP4(g(e,e),w,b)
| ~ ld__(w,w) ),
inference(superposition,[status(thm)],[c_4460,c_192]) ).
tcf(c_5582,plain,
( ~ ld__(c,k)
| ~ ld__(c,c) ),
inference(superposition,[status(thm)],[c_5293,c_187]) ).
tcf(c_5583,plain,
~ ld__(c,c),
inference(forward_subsumption_resolution,[status(thm)],[c_5582,c_2295]) ).
tcf(c_5743,plain,
( sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5028,c_5736]) ).
tcf(c_5830,plain,
( sP3(h(d),g(e,e),k)
| sP4(h(d),g(e,e),k) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5079,c_5823]) ).
tcf(c_5941,plain,
( sP4(h(d),g(e,e),k)
| ~ ld__(k,c) ),
inference(superposition,[status(thm)],[c_5743,c_190]) ).
tcf(c_5944,plain,
sP4(h(d),g(e,e),k),
inference(forward_subsumption_resolution,[status(thm)],[c_5941,c_154]) ).
tcf(c_5952,plain,
( sP4(g(e,e),w,b)
| ~ ld__(w,w)
| ~ ld__(w,b) ),
inference(superposition,[status(thm)],[c_5357,c_189]) ).
tcf(c_5954,plain,
( sP4(g(e,e),w,b)
| ~ ld__(w,w) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5952,c_142]) ).
tcf(c_6002,plain,
( ~ ld__(lkg,lkg)
| sP4(k,lkg,hill) ),
inference(global_subsumption_just,[status(thm)],[c_5332,c_5419]) ).
tcf(c_6003,plain,
( sP4(k,lkg,hill)
| ~ ld__(lkg,lkg) ),
inference(renaming,[status(thm)],[c_6002]) ).
tcf(c_6009,plain,
( ~ ld__(hill,k)
| ~ ld__(lkg,lkg) ),
inference(superposition,[status(thm)],[c_6003,c_187]) ).
tcf(c_6010,plain,
~ ld__(lkg,lkg),
inference(forward_subsumption_resolution,[status(thm)],[c_6009,c_180]) ).
tcf(c_6042,plain,
( ~ ld__(c,k)
| ~ ld__(b,b) ),
inference(superposition,[status(thm)],[c_5294,c_187]) ).
tcf(c_6043,plain,
~ ld__(b,b),
inference(forward_subsumption_resolution,[status(thm)],[c_6042,c_2295]) ).
tcf(c_6044,plain,
sP4(h(d),g(e,e),k),
inference(global_subsumption_just,[status(thm)],[c_5830,c_5944]) ).
tcf(c_6046,plain,
~ ld__(h(d),h(d)),
inference(superposition,[status(thm)],[c_6044,c_185]) ).
tcf(c_6047,plain,
~ ld__(k,k),
inference(superposition,[status(thm)],[c_6044,c_187]) ).
tcf(c_6048,plain,
( ~ ld__(w,w)
| sP4(g(e,e),w,b) ),
inference(global_subsumption_just,[status(thm)],[c_5490,c_5954]) ).
tcf(c_6049,plain,
( sP4(g(e,e),w,b)
| ~ ld__(w,w) ),
inference(renaming,[status(thm)],[c_6048]) ).
tcf(c_6055,plain,
( ~ ld__(w,w)
| ~ ld__(b,k) ),
inference(superposition,[status(thm)],[c_6049,c_187]) ).
tcf(c_6056,plain,
~ ld__(w,w),
inference(forward_subsumption_resolution,[status(thm)],[c_6055,c_2284]) ).
tcf(c_6111,plain,
( ~ ld__(hill,hill)
| sP4(k,lkg,hill) ),
inference(global_subsumption_just,[status(thm)],[c_5346,c_5438]) ).
tcf(c_6112,plain,
( sP4(k,lkg,hill)
| ~ ld__(hill,hill) ),
inference(renaming,[status(thm)],[c_6111]) ).
tcf(c_6118,plain,
( ~ ld__(hill,hill)
| ~ ld__(hill,k) ),
inference(superposition,[status(thm)],[c_6112,c_187]) ).
tcf(c_6119,plain,
~ ld__(hill,hill),
inference(forward_subsumption_resolution,[status(thm)],[c_6118,c_180]) ).
tcf(c_6120,plain,
~ ld__(d,d),
inference(superposition,[status(thm)],[c_3990,c_6046]) ).
tcf(c_6122,plain,
~ ld__(lkg,lkg),
inference(global_subsumption_just,[status(thm)],[c_5419,c_6010]) ).
tcf(c_6124,plain,
~ ld__(hill,hill),
inference(global_subsumption_just,[status(thm)],[c_5438,c_6119]) ).
tcf(c_6189,plain,
sP3(a,b,c),
inference(backward_subsumption_resolution,[status(thm)],[c_5288,c_4797]) ).
tcf(c_6199,plain,
( sP2(g(e,e),w,b)
| sP3(g(e,e),w,b) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4460,c_4802]) ).
tcf(c_6226,plain,
~ ld__(e,e),
inference(superposition,[status(thm)],[c_6044,c_4794]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MSC016+1 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p SAT
% 0.08/0.36 % Computer : n003.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 01:32:21 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p SAT
% 0.08/0.40 Running model finding
% 0.08/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fnt_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.41
% 0.08/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.08/0.41
% 0.08/0.41 % Detected problem language: tptp
% 0.08/0.42 % Proving...
% 7.59/1.77 % SZS status Started for theBenchmark.p
% 7.59/1.77 % SZS status CounterSatisfiable for theBenchmark.p
% 7.59/1.77
% 7.59/1.77 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.59/1.77
% 7.59/1.77 ------ iProver source info
% 7.59/1.77
% 7.59/1.77 git: date: 2026-07-19 20:42:38 +0200
% 7.59/1.77 git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.59/1.77 git: non_committed_changes: false
% 7.59/1.77
% 7.59/1.77 ------ Parsing...
% 7.59/1.77 ------ Clausification by vclausify_rel & Parsing by iProver...
% 7.59/1.77 ------ Proving...
% 7.59/1.77 ------ Problem Properties
% 7.59/1.77
% 7.59/1.77
% 7.59/1.77 clauses 154
% 7.59/1.77 conjectures 3
% 7.59/1.77 EPR 101
% 7.59/1.77 Horn 151
% 7.59/1.77 unary 132
% 7.59/1.77 binary 19
% 7.59/1.77 lits 191
% 7.59/1.77 lits eq 0
% 7.59/1.77 fd_pure 0
% 7.59/1.77 fd_pseudo 0
% 7.59/1.77 fd_cond 0
% 7.59/1.77 fd_pseudo_cond 0
% 7.59/1.77 AC symbols 0
% 7.59/1.77
% 7.59/1.77 ------ Schedule dynamic 5 is on
% 7.59/1.77
% 7.59/1.77 ------ no equalities: superposition off
% 7.59/1.77
% 7.59/1.77 ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 7.59/1.77
% 7.59/1.77
% 7.59/1.77 ------
% 7.59/1.77 Current options:
% 7.59/1.77 ------
% 7.59/1.77
% 7.59/1.77 ------ Input Options
% 7.59/1.77
% 7.59/1.77 --out_options all
% 7.59/1.77 --tptp_safe_out true
% 7.59/1.77 --problem_path ""
% 7.59/1.77 --include_path ""
% 7.59/1.77 --clausifier res/vclausify_rel
% 7.59/1.77 --clausifier_options --mode clausify -t 101.67 -updr off
% 7.59/1.77 --stdin false
% 7.59/1.77 --proof_out true
% 7.59/1.77 --proof_dot_file ""
% 7.59/1.77 --proof_reduce_dot []
% 7.59/1.77 --suppress_sat_res false
% 7.59/1.77 --suppress_unsat_res true
% 7.59/1.77 --stats_out none
% 7.59/1.77 --stats_mem false
% 7.59/1.77 --theory_stats_out false
% 7.59/1.77
% 7.59/1.77 ------ General Options
% 7.59/1.77
% 7.59/1.77 --fof false
% 7.59/1.77 --time_out_real 305.
% 7.59/1.77 --time_out_virtual -1.
% 7.59/1.77 --rnd_seed 13
% 7.59/1.77 --symbol_type_check false
% 7.59/1.77 --clausify_out false
% 7.59/1.77 --sig_cnt_out false
% 7.59/1.77 --trig_cnt_out false
% 7.59/1.77 --trig_cnt_out_tolerance 1.
% 7.59/1.77 --trig_cnt_out_sk_spl false
% 7.59/1.77 --abstr_cl_out false
% 7.59/1.77
% 7.59/1.77 ------ Interactive Mode
% 7.59/1.77
% 7.59/1.77 --interactive_mode false
% 7.59/1.77 --external_ip_address ""
% 7.59/1.77 --external_port 0
% 7.59/1.77
% 7.59/1.77 ------ Global Options
% 7.59/1.77
% 7.59/1.77 --schedule default
% 7.59/1.77 --add_important_lit false
% 7.59/1.77 --prop_solver_per_cl 500
% 7.59/1.77 --subs_bck_mult 8
% 7.59/1.77 --min_unsat_core false
% 7.59/1.77 --soft_assumptions false
% 7.59/1.77 --soft_lemma_size 3
% 7.59/1.77 --prop_impl_unit_size 0
% 7.59/1.77 --prop_impl_unit []
% 7.59/1.77 --share_sel_clauses true
% 7.59/1.77 --reset_solvers false
% 7.59/1.77 --bc_imp_inh [conj_cone]
% 7.59/1.77 --conj_cone_tolerance 3.
% 7.59/1.77 --extra_neg_conj none
% 7.59/1.77 --large_theory_mode true
% 7.59/1.77 --prolific_symb_bound 200
% 7.59/1.77 --lt_threshold 2000
% 7.59/1.77 --clause_weak_htbl true
% 7.59/1.77 --gc_record_bc_elim false
% 7.59/1.77
% 7.59/1.77 ------ Preprocessing Options
% 7.59/1.77
% 7.59/1.77 --preprocessing_flag false
% 7.59/1.77 --time_out_prep_mult 0.1
% 7.59/1.77 --splitting_mode input
% 7.59/1.77 --splitting_grd true
% 7.59/1.77 --splitting_cvd false
% 7.59/1.77 --splitting_cvd_svl false
% 7.59/1.77 --splitting_nvd 32
% 7.59/1.77 --sub_typing false
% 7.59/1.77 --prep_eq_flat_conj false
% 7.59/1.77 --prep_ineq_split false
% 7.59/1.77 --prep_eq_flat_all_gr false
% 7.59/1.77 --prep_gs_sim true
% 7.59/1.77 --prep_unflatten true
% 7.59/1.77 --prep_res_sim true
% 7.59/1.77 --prep_sup_sim_all true
% 7.59/1.77 --prep_sup_sim_sup false
% 7.59/1.77 --prep_upred true
% 7.59/1.77 --prep_well_definedness true
% 7.59/1.77 --prep_sem_filter exhaustive
% 7.59/1.77 --prep_sem_filter_out false
% 7.59/1.77 --pred_elim true
% 7.59/1.77 --res_sim_input true
% 7.59/1.77 --eq_ax_congr_red true
% 7.59/1.77 --pure_diseq_elim true
% 7.59/1.77 --brand_transform false
% 7.59/1.77 --non_eq_to_eq false
% 7.59/1.77 --prep_eq_proxy false
% 7.59/1.77 --prep_def_merge true
% 7.59/1.77 --prep_def_merge_prop_impl false
% 7.59/1.77 --prep_def_merge_mbd true
% 7.59/1.77 --prep_def_merge_tr_red false
% 7.59/1.77 --prep_def_merge_tr_cl false
% 7.59/1.77 --smt_preprocessing false
% 7.59/1.77 --smt_ac_axioms fast
% 7.59/1.77 --preprocessed_out false
% 7.59/1.77 --preprocessed_stats false
% 7.59/1.77
% 7.59/1.77 ------ Abstraction refinement Options
% 7.59/1.77
% 7.59/1.77 --abstr_ref []
% 7.59/1.77 --abstr_ref_prep false
% 7.59/1.77 --abstr_ref_until_sat false
% 7.59/1.77 --abstr_ref_sig_restrict funpre
% 7.59/1.77 --abstr_ref_af_restrict_to_split_sk false
% 7.59/1.77 --abstr_ref_under []
% 7.59/1.77
% 7.59/1.77 ------ SAT Options
% 7.59/1.77
% 7.59/1.77 --sat_mode false
% 7.59/1.77 --sat_fm_restart_options ""
% 7.59/1.77 --sat_gr_def false
% 7.59/1.77 --sat_epr_types true
% 7.59/1.77 --sat_non_cyclic_types false
% 7.59/1.77 --sat_finite_models false
% 7.59/1.77 --sat_fm_lemmas false
% 7.59/1.77 --sat_fm_prep false
% 7.59/1.77 --sat_fm_uc_incr true
% 7.59/1.77 --sat_out_model pos
% 7.59/1.77 --sat_out_clauses false
% 7.59/1.77
% 7.59/1.77 ------ QBF Options
% 7.59/1.77
% 7.59/1.77 --qbf_mode false
% 7.59/1.77 --qbf_elim_univ false
% 7.59/1.77 --qbf_dom_inst none
% 7.59/1.77 --qbf_dom_pre_inst false
% 7.59/1.77 --qbf_sk_in false
% 7.59/1.77 --qbf_pred_elim true
% 7.59/1.77 --qbf_split 512
% 7.59/1.77
% 7.59/1.77 ------ BMC1 Options
% 7.59/1.77
% 7.59/1.77 --bmc1_incremental false
% 7.59/1.77 --bmc1_axioms reachable_all
% 7.59/1.77 --bmc1_min_bound 0
% 7.59/1.77 --bmc1_max_bound -1
% 7.59/1.77 --bmc1_max_bound_default -1
% 7.59/1.77 --bmc1_symbol_reachability true
% 7.59/1.77 --bmc1_property_lemmas false
% 7.59/1.77 --bmc1_k_induction false
% 7.59/1.77 --bmc1_non_equiv_states false
% 7.59/1.77 --bmc1_deadlock false
% 7.59/1.77 --bmc1_ucm false
% 7.59/1.77 --bmc1_add_unsat_core none
% 7.59/1.77 --bmc1_unsat_core_children false
% 7.59/1.77 --bmc1_unsat_core_extrapolate_axioms false
% 7.59/1.77 --bmc1_out_stat full
% 7.59/1.77 --bmc1_ground_init false
% 7.59/1.77 --bmc1_pre_inst_next_state false
% 7.59/1.77 --bmc1_pre_inst_state false
% 7.59/1.77 --bmc1_pre_inst_reach_state false
% 7.59/1.77 --bmc1_out_unsat_core false
% 7.59/1.77 --bmc1_aig_witness_out false
% 7.59/1.77 --bmc1_verbose false
% 7.59/1.77 --bmc1_dump_clauses_tptp false
% 7.59/1.77 --bmc1_dump_unsat_core_tptp false
% 7.59/1.77 --bmc1_dump_file -
% 7.59/1.77 --bmc1_ucm_expand_uc_limit 128
% 7.59/1.77 --bmc1_ucm_n_expand_iterations 6
% 7.59/1.77 --bmc1_ucm_extend_mode 1
% 7.59/1.77 --bmc1_ucm_init_mode 2
% 7.59/1.77 --bmc1_ucm_cone_mode none
% 7.59/1.77 --bmc1_ucm_reduced_relation_type 0
% 7.59/1.77 --bmc1_ucm_relax_model 4
% 7.59/1.77 --bmc1_ucm_full_tr_after_sat true
% 7.59/1.77 --bmc1_ucm_expand_neg_assumptions false
% 7.59/1.77 --bmc1_ucm_layered_model none
% 7.59/1.77 --bmc1_ucm_max_lemma_size 10
% 7.59/1.77
% 7.59/1.77 ------ AIG Options
% 7.59/1.77
% 7.59/1.77 --aig_mode false
% 7.59/1.77
% 7.59/1.77 ------ Instantiation Options
% 7.59/1.77
% 7.59/1.77 --instantiation_flag true
% 7.59/1.77 --inst_sos_flag false
% 7.59/1.77 --inst_sos_phase true
% 7.59/1.77 --inst_sos_sth_lit_sel [+prop;+non_prol_conj_symb;-eq;+ground;-num_var;-num_symb]
% 7.59/1.77 --inst_lit_sel [+prop;+sign;+ground;-num_var;-num_symb]
% 7.59/1.77 --inst_lit_sel_side none
% 7.59/1.77 --inst_solver_per_active 1400
% 7.59/1.77 --inst_solver_calls_frac 1.
% 7.59/1.77 --inst_to_smt_solver true
% 7.59/1.77 --inst_passive_queue_type priority_queues
% 7.59/1.77 --inst_passive_queues [[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]
% 7.59/1.77 --inst_passive_queues_freq [25;2]
% 7.59/1.77 --inst_dismatching true
% 7.59/1.77 --inst_eager_unprocessed_to_passive true
% 7.59/1.77 --inst_unprocessed_bound 1000
% 7.59/1.77 --inst_prop_sim_given true
% 7.59/1.77 --inst_prop_sim_new false
% 7.59/1.77 --inst_subs_new false
% 7.59/1.77 --inst_eq_res_simp false
% 7.59/1.77 --inst_subs_given false
% 7.59/1.77 --inst_orphan_elimination true
% 7.59/1.77 --inst_learning_loop_flag true
% 7.59/1.77 --inst_learning_start 3000
% 7.59/1.77 --inst_learning_factor 2
% 7.59/1.77 --inst_start_prop_sim_after_learn 3
% 7.59/1.77 --inst_sel_renew solver
% 7.59/1.77 --inst_lit_activity_flag true
% 7.59/1.77 --inst_restr_to_given false
% 7.59/1.77 --inst_activity_threshold 500
% 7.59/1.77
% 7.59/1.77 ------ Resolution Options
% 7.59/1.77
% 7.59/1.77 --resolution_flag false
% 7.59/1.77 --res_lit_sel adaptive
% 7.59/1.77 --res_lit_sel_side none
% 7.59/1.77 --res_ordering kbo
% 7.59/1.77 --res_to_prop_solver active
% 7.59/1.77 --res_prop_simpl_new false
% 7.59/1.77 --res_prop_simpl_given true
% 7.59/1.77 --res_to_smt_solver true
% 7.59/1.77 --res_passive_queue_type priority_queues
% 7.59/1.77 --res_passive_queues [[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]
% 7.59/1.77 --res_passive_queues_freq [15;5]
% 7.59/1.77 --res_forward_subs full
% 7.59/1.77 --res_backward_subs full
% 7.59/1.77 --res_forward_subs_resolution true
% 7.59/1.77 --res_backward_subs_resolution true
% 7.59/1.77 --res_orphan_elimination true
% 7.59/1.77 --res_time_limit 300.
% 7.59/1.77
% 7.59/1.77 ------ Superposition Options
% 7.59/1.77
% 7.59/1.77 --superposition_flag true
% 7.59/1.77 --sup_passive_queue_type priority_queues
% 7.59/1.77 --sup_passive_queues [[-conj_dist;-num_symb];[+score;+min_def_symb;-max_atom_input_occur;+conj_non_prolific_symb];[+age;-num_symb];[+score;-num_symb]]
% 7.59/1.77 --sup_passive_queues_freq [8;1;4;4]
% 7.59/1.77 --twee_lhs_weight 4
% 7.59/1.77 --sup_set_join false
% 7.59/1.77 --sup_set_join_goals true
% 7.59/1.77 --sup_set_join_limit 1000
% 7.59/1.77 --demod_completeness_check fast
% 7.59/1.77 --demod_use_ground true
% 7.59/1.77 --sup_unprocessed_bound 0
% 7.59/1.77 --sup_to_prop_solver passive
% 7.59/1.77 --sup_prop_simpl_new true
% 7.59/1.77 --sup_prop_simpl_given true
% 7.59/1.77 --sup_fun_splitting false
% 7.59/1.77 --sup_iter_deepening 2
% 7.59/1.77 --sup_restarts_mult 12
% 7.59/1.77 --sup_score sim_d_gen
% 7.59/1.77 --sup_share_score_frac 0.2
% 7.59/1.77 --sup_share_max_num_cl 500
% 7.59/1.77 --sup_ordering kbo
% 7.59/1.77 --sup_symb_ordering invfreq
% 7.59/1.77 --sup_term_weight default
% 7.59/1.77
% 7.59/1.77 ------ Superposition Simplification Setup
% 7.59/1.77
% 7.59/1.77 --sup_indices_passive [LightNormIndex;FwDemodIndex]
% 7.59/1.77 --sup_full_triv [SMTSimplify;PropSubs]
% 7.59/1.77 --sup_full_fw [ACNormalisation;FwLightNorm;FwDemod;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes;FwGroundJoinability]
% 7.59/1.77 --sup_full_bw [BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 7.59/1.77 --sup_immed_triv []
% 7.59/1.77 --sup_immed_fw_main [ACNormalisation;FwLightNorm;FwUnitSubsAndRes]
% 7.59/1.77 --sup_immed_fw_immed [ACNormalisation;FwUnitSubsAndRes]
% 7.59/1.77 --sup_immed_bw_main [BwUnitSubsAndRes;BwDemod]
% 7.59/1.77 --sup_immed_bw_immed [BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 7.59/1.77 --sup_input_triv [Unflattening;SMTSimplify]
% 7.59/1.77 --sup_input_fw [FwACDemod;ACNormalisation;FwLightNorm;FwDemod;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes;FwGroundJoinability]
% 7.59/1.77 --sup_input_bw [BwACDemod;BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 7.59/1.77 --sup_full_fixpoint true
% 7.59/1.77 --sup_main_fixpoint true
% 7.59/1.77 --sup_immed_fixpoint false
% 7.59/1.77 --sup_input_fixpoint true
% 7.59/1.77 --sup_cache_sim none
% 7.59/1.77 --sup_smt_interval 500
% 7.59/1.77 --sup_bw_gjoin_interval 0
% 7.59/1.77
% 7.59/1.77 ------ Combination Options
% 7.59/1.77
% 7.59/1.77 --comb_mode clause_based
% 7.59/1.77 --comb_inst_mult 5
% 7.59/1.77 --comb_res_mult 1
% 7.59/1.77 --comb_sup_mult 1
% 7.59/1.77 --comb_sup_deep_mult 1
% 7.59/1.77
% 7.59/1.77 ------ Debug Options
% 7.59/1.77
% 7.59/1.77 --dbg_backtrace false
% 7.59/1.77 --dbg_dump_prop_clauses false
% 7.59/1.77 --dbg_dump_prop_clauses_file -
% 7.59/1.77 --dbg_out_stat false
% 7.59/1.77 --dbg_just_parse false
% 7.59/1.77
% 7.59/1.77
% 7.59/1.77
% 7.59/1.77
% 7.59/1.77 ------ Proving...
% 7.59/1.77
% 7.59/1.77
% 7.59/1.77 % SZS status CounterSatisfiable for theBenchmark.p
% 7.59/1.77
% 7.59/1.77 % SZS output start Saturation for theBenchmark.p
% See solution above
% 7.59/1.79
% 7.59/1.79
%------------------------------------------------------------------------------