%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : AGT005+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 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 12:50:45 PM UTC 2026
% Result : Theorem 13.21s 2.31s
% Output : Proof 13.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 54
% Syntax : Number of formulae : 241 ( 217 unt; 0 def)
% Number of atoms : 306 ( 33 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 282 ( 217 ~; 43 |; 17 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-4 aty)
% Number of functors : 26 ( 26 usr; 23 con; 0-4 aty)
% Number of variables : 101 ( 12 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f549,axiom,
! [X,Y,RDN_X,RDN_Y] :
( ( rdn_positive_less(RDN_X,RDN_Y)
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_translate(X,rdn_pos(RDN_X)) )
=> less(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_entry_point_pos_pos) ).
fof(f549_nnf,plain,
! [X,Y,RDN_X,RDN_Y] :
( less(X,Y)
| ~ rdn_positive_less(RDN_X,RDN_Y)
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ),
inference(nnf_transformation,[status(thm)],[f549]) ).
fof(f549_sk,plain,
! [X,RDN_X,Y,RDN_Y] :
( less(X,Y)
| ~ rdn_positive_less(RDN_X,RDN_Y)
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ),
inference(skolemisation,[status(esa)],[f549_nnf]) ).
cnf(c618,plain,
( less(X0,X1)
| ~ rdn_positive_less(X2,X3)
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X2)) ),
inference(cnf_transformation,[status(esa)],[f549_sk]) ).
cnf(hi577,axiom,
ifeq(rdn_translate(X0,rdn_pos(X1)),true,ifeq(rdn_translate(X2,rdn_pos(X3)),true,ifeq(rdn_positive_less(X1,X3),true,less(X0,X2),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c618]) ).
fof(f272,axiom,
rdn_translate(n3,rdn_pos(rdnn(n3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rdn3) ).
fof(f272_nnf,plain,
rdn_translate(n3,rdn_pos(rdnn(n3))),
inference(nnf_transformation,[status(thm)],[f272]) ).
cnf(c341,plain,
rdn_translate(n3,rdn_pos(rdnn(n3))),
inference(cnf_transformation,[status(esa)],[f272_nnf]) ).
cnf(hi300,axiom,
rdn_translate(n3,rdn_pos(rdnn(n3))) = true,
inference(equality_encoding,[status(esa)],[c341]) ).
fof(f273,axiom,
rdn_translate(n4,rdn_pos(rdnn(n4))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rdn4) ).
fof(f273_nnf,plain,
rdn_translate(n4,rdn_pos(rdnn(n4))),
inference(nnf_transformation,[status(thm)],[f273]) ).
cnf(c342,plain,
rdn_translate(n4,rdn_pos(rdnn(n4))),
inference(cnf_transformation,[status(esa)],[f273_nnf]) ).
cnf(hi301,axiom,
rdn_translate(n4,rdn_pos(rdnn(n4))) = true,
inference(equality_encoding,[status(esa)],[c342]) ).
fof(f537,axiom,
rdn_positive_less(rdnn(n3),rdnn(n4)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rdn_positive_less34) ).
fof(f537_nnf,plain,
rdn_positive_less(rdnn(n3),rdnn(n4)),
inference(nnf_transformation,[status(thm)],[f537]) ).
cnf(c606,plain,
rdn_positive_less(rdnn(n3),rdnn(n4)),
inference(cnf_transformation,[status(esa)],[f537_nnf]) ).
cnf(hi565,axiom,
rdn_positive_less(rdnn(n3),rdnn(n4)) = true,
inference(equality_encoding,[status(esa)],[c606]) ).
cnf(h7658,plain,
less(n3,n4) = true,
inference(hyper_resolution,[status(thm)],[hi577,hi300,hi301,hi565]) ).
fof(f274,axiom,
rdn_translate(n5,rdn_pos(rdnn(n5))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rdn5) ).
fof(f274_nnf,plain,
rdn_translate(n5,rdn_pos(rdnn(n5))),
inference(nnf_transformation,[status(thm)],[f274]) ).
cnf(c343,plain,
rdn_translate(n5,rdn_pos(rdnn(n5))),
inference(cnf_transformation,[status(esa)],[f274_nnf]) ).
cnf(hi302,axiom,
rdn_translate(n5,rdn_pos(rdnn(n5))) = true,
inference(equality_encoding,[status(esa)],[c343]) ).
fof(f538,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rdn_positive_less45) ).
fof(f538_nnf,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(nnf_transformation,[status(thm)],[f538]) ).
cnf(c607,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(cnf_transformation,[status(esa)],[f538_nnf]) ).
cnf(hi566,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)) = true,
inference(equality_encoding,[status(esa)],[c607]) ).
cnf(h7685,plain,
less(n4,n5) = true,
inference(hyper_resolution,[status(thm)],[hi577,hi301,hi302,hi566]) ).
fof(f0,axiom,
! [A,C,N,L] :
( accept_team(A,L,C,N)
<=> ( accept_number(A,N)
& accept_leader(A,L)
& accept_city(A,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1_1) ).
fof(f0_nnf,plain,
! [A,C,N,L] :
( ( ~ accept_number(A,N)
| ~ accept_leader(A,L)
| ~ accept_city(A,C)
| accept_team(A,L,C,N) )
& ( ( accept_number(A,N)
& accept_leader(A,L)
& accept_city(A,C) )
| ~ accept_team(A,L,C,N) ) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,L,C,N] :
( ( ~ accept_number(A,N)
| ~ accept_leader(A,L)
| ~ accept_city(A,C)
| accept_team(A,L,C,N) )
& ( ( accept_number(A,N)
& accept_leader(A,L)
& accept_city(A,C) )
| ~ accept_team(A,L,C,N) ) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c2,plain,
( accept_number(X0,X2)
| ~ accept_team(X0,X3,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi2,axiom,
ifeq(accept_team(X0,X1,X2,X3),true,accept_number(X0,X3),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
fof(f109,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_90) ).
fof(f109_nnf,plain,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n5),
inference(nnf_transformation,[status(thm)],[f109]) ).
cnf(c178,plain,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n5),
inference(cnf_transformation,[status(esa)],[f109_nnf]) ).
cnf(hi164,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n5) = true,
inference(equality_encoding,[status(esa)],[c178]) ).
cnf(h1639,plain,
accept_number(christiansufferterrahumanitarianorganization,n5) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi164]) ).
fof(f1,axiom,
! [A,N,M] :
( ( less(M,N)
& accept_number(A,N) )
=> accept_number(A,M) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1_2) ).
fof(f1_nnf,plain,
! [A,N,M] :
( accept_number(A,M)
| ~ less(M,N)
| ~ accept_number(A,N) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,N,M] :
( accept_number(A,M)
| ~ less(M,N)
| ~ accept_number(A,N) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c4,plain,
( accept_number(X0,X2)
| ~ less(X2,X1)
| ~ accept_number(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi4,axiom,
ifeq(accept_number(X0,X1),true,ifeq(less(X2,X1),true,accept_number(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h7715,plain,
accept_number(christiansufferterrahumanitarianorganization,n4) = true,
inference(hyper_resolution,[status(thm)],[hi4,h1639,h7685]) ).
cnf(h7746,plain,
accept_number(christiansufferterrahumanitarianorganization,n3) = true,
inference(hyper_resolution,[status(thm)],[hi4,h7715,h7658]) ).
cnf(c1,plain,
( accept_leader(X0,X3)
| ~ accept_team(X0,X3,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi1,axiom,
ifeq(accept_team(X0,X1,X2,X3),true,accept_leader(X0,X1),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
fof(f112,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,coastvillage,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_93) ).
fof(f112_nnf,plain,
accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,coastvillage,n6),
inference(nnf_transformation,[status(thm)],[f112]) ).
cnf(c181,plain,
accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,coastvillage,n6),
inference(cnf_transformation,[status(esa)],[f112_nnf]) ).
cnf(hi167,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,coastvillage,n6) = true,
inference(equality_encoding,[status(esa)],[c181]) ).
cnf(h1666,plain,
accept_leader(christiansufferterrahumanitarianorganization,countryafirstaidorganization) = true,
inference(hyper_resolution,[status(thm)],[hi1,hi167]) ).
cnf(c0,plain,
( accept_city(X0,X1)
| ~ accept_team(X0,X3,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(accept_team(X0,X1,X2,X3),true,accept_city(X0,X2),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
fof(f45,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,towna,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_26) ).
fof(f45_nnf,plain,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,towna,n6),
inference(nnf_transformation,[status(thm)],[f45]) ).
cnf(c114,plain,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,towna,n6),
inference(cnf_transformation,[status(esa)],[f45_nnf]) ).
cnf(hi111,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,towna,n6) = true,
inference(equality_encoding,[status(esa)],[c114]) ).
cnf(h1302,plain,
accept_city(christiansufferterrahumanitarianorganization,towna) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi111]) ).
cnf(c3,plain,
( ~ accept_number(X0,X2)
| ~ accept_leader(X0,X3)
| ~ accept_city(X0,X1)
| accept_team(X0,X3,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi3,axiom,
ifeq(accept_city(X0,X1),true,ifeq(accept_leader(X0,X2),true,ifeq(accept_number(X0,X3),true,accept_team(X0,X2,X1,X3),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(h7879,plain,
accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,towna,n3) = true,
inference(hyper_resolution,[status(thm)],[hi3,h1302,h1666,h7746]) ).
fof(f555,conjecture,
accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,towna,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query_5) ).
fof(f555_neg,negated_conjecture,
~ accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,towna,n3),
inference(negated_conjecture,[status(cth)],[f555]) ).
fof(f555_nnf,plain,
~ accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,towna,n3),
inference(nnf_transformation,[status(thm)],[f555_neg]) ).
fof(f555_sk,plain,
~ accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,towna,n3),
inference(skolemisation,[status(esa)],[f555_nnf]) ).
cnf(c628,plain,
~ accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,towna,n3),
inference(cnf_transformation,[status(esa)],[f555_sk]) ).
cnf(hi628,negated_conjecture,
ifeq(accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,towna,n3),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c628]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi628,h7879]) ).
cnf(t351,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f5,axiom,
! [A,L,C] :
( the_agent_not_in_any_proposed_teams(A,L,C)
=> ~ ( accept_leader(A,L)
& accept_city(A,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1_6) ).
fof(f5_nnf,plain,
! [A,L,C] :
( ~ accept_leader(A,L)
| ~ accept_city(A,C)
| ~ the_agent_not_in_any_proposed_teams(A,L,C) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,L,C] :
( ~ accept_leader(A,L)
| ~ accept_city(A,C)
| ~ the_agent_not_in_any_proposed_teams(A,L,C) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c9,plain,
( ~ accept_leader(X0,X1)
| ~ accept_city(X0,X2)
| ~ the_agent_not_in_any_proposed_teams(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
fof(f28,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_9) ).
fof(f28_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n4),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n4),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c97,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n4),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
fof(f29,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_10) ).
fof(f29_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n5),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n5),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c98,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n5),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
fof(f48,axiom,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_29) ).
fof(f48_nnf,plain,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n2),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n2),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c117,plain,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n2),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
fof(f49,axiom,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_30) ).
fof(f49_nnf,plain,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n2),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n2),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c118,plain,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n2),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
fof(f50,axiom,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_31) ).
fof(f50_nnf,plain,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n2),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n2),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c119,plain,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n2),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
fof(f51,axiom,
~ accept_team(countryamedicalorganization,christiansufferterrahumanitarianorganization,coastvillage,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_32) ).
fof(f51_nnf,plain,
~ accept_team(countryamedicalorganization,christiansufferterrahumanitarianorganization,coastvillage,n2),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
~ accept_team(countryamedicalorganization,christiansufferterrahumanitarianorganization,coastvillage,n2),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c120,plain,
~ accept_team(countryamedicalorganization,christiansufferterrahumanitarianorganization,coastvillage,n2),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
fof(f52,axiom,
~ accept_team(countryamedicalorganization,sufferterragovernment,coastvillage,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_33) ).
fof(f52_nnf,plain,
~ accept_team(countryamedicalorganization,sufferterragovernment,coastvillage,n2),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
~ accept_team(countryamedicalorganization,sufferterragovernment,coastvillage,n2),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c121,plain,
~ accept_team(countryamedicalorganization,sufferterragovernment,coastvillage,n2),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
fof(f53,axiom,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_34) ).
fof(f53_nnf,plain,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n6),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n6),
inference(skolemisation,[status(esa)],[f53_nnf]) ).
cnf(c122,plain,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n6),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
fof(f54,axiom,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_35) ).
fof(f54_nnf,plain,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n6),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n6),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c123,plain,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n6),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
fof(f55,axiom,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_36) ).
fof(f55_nnf,plain,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n6),
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n6),
inference(skolemisation,[status(esa)],[f55_nnf]) ).
cnf(c124,plain,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n6),
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
fof(f59,axiom,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_40) ).
fof(f59_nnf,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c128,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
fof(f90,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_71) ).
fof(f90_nnf,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n5),
inference(nnf_transformation,[status(thm)],[f90]) ).
fof(f90_sk,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n5),
inference(skolemisation,[status(esa)],[f90_nnf]) ).
cnf(c159,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n5),
inference(cnf_transformation,[status(esa)],[f90_sk]) ).
fof(f91,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_72) ).
fof(f91_nnf,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n6),
inference(nnf_transformation,[status(thm)],[f91]) ).
fof(f91_sk,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n6),
inference(skolemisation,[status(esa)],[f91_nnf]) ).
cnf(c160,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n6),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
fof(f134,axiom,
~ accept_team(countryccivilorganization,muslimcountrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_115) ).
fof(f134_nnf,plain,
~ accept_team(countryccivilorganization,muslimcountrybhumanitarianorganization,townc,n6),
inference(nnf_transformation,[status(thm)],[f134]) ).
fof(f134_sk,plain,
~ accept_team(countryccivilorganization,muslimcountrybhumanitarianorganization,townc,n6),
inference(skolemisation,[status(esa)],[f134_nnf]) ).
cnf(c203,plain,
~ accept_team(countryccivilorganization,muslimcountrybhumanitarianorganization,townc,n6),
inference(cnf_transformation,[status(esa)],[f134_sk]) ).
fof(f135,axiom,
~ accept_team(countryccivilorganization,countrybcivilorganization,townc,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_116) ).
fof(f135_nnf,plain,
~ accept_team(countryccivilorganization,countrybcivilorganization,townc,n6),
inference(nnf_transformation,[status(thm)],[f135]) ).
fof(f135_sk,plain,
~ accept_team(countryccivilorganization,countrybcivilorganization,townc,n6),
inference(skolemisation,[status(esa)],[f135_nnf]) ).
cnf(c204,plain,
~ accept_team(countryccivilorganization,countrybcivilorganization,townc,n6),
inference(cnf_transformation,[status(esa)],[f135_sk]) ).
fof(f136,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_117) ).
fof(f136_nnf,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,townc,n6),
inference(nnf_transformation,[status(thm)],[f136]) ).
fof(f136_sk,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,townc,n6),
inference(skolemisation,[status(esa)],[f136_nnf]) ).
cnf(c205,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,townc,n6),
inference(cnf_transformation,[status(esa)],[f136_sk]) ).
fof(f137,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,townc,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_118) ).
fof(f137_nnf,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,townc,n6),
inference(nnf_transformation,[status(thm)],[f137]) ).
fof(f137_sk,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,townc,n6),
inference(skolemisation,[status(esa)],[f137_nnf]) ).
cnf(c206,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,townc,n6),
inference(cnf_transformation,[status(esa)],[f137_sk]) ).
fof(f138,axiom,
~ accept_team(countryccivilorganization,countrycmedicalorganization,townc,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_119) ).
fof(f138_nnf,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,townc,n6),
inference(nnf_transformation,[status(thm)],[f138]) ).
fof(f138_sk,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,townc,n6),
inference(skolemisation,[status(esa)],[f138_nnf]) ).
cnf(c207,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,townc,n6),
inference(cnf_transformation,[status(esa)],[f138_sk]) ).
fof(f162,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_143) ).
fof(f162_nnf,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n5),
inference(nnf_transformation,[status(thm)],[f162]) ).
fof(f162_sk,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n5),
inference(skolemisation,[status(esa)],[f162_nnf]) ).
cnf(c231,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n5),
inference(cnf_transformation,[status(esa)],[f162_sk]) ).
fof(f163,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_144) ).
fof(f163_nnf,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n6),
inference(nnf_transformation,[status(thm)],[f163]) ).
fof(f163_sk,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n6),
inference(skolemisation,[status(esa)],[f163_nnf]) ).
cnf(c232,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n6),
inference(cnf_transformation,[status(esa)],[f163_sk]) ).
fof(f193,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_174) ).
fof(f193_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n2),
inference(nnf_transformation,[status(thm)],[f193]) ).
fof(f193_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n2),
inference(skolemisation,[status(esa)],[f193_nnf]) ).
cnf(c262,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n2),
inference(cnf_transformation,[status(esa)],[f193_sk]) ).
fof(f194,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_175) ).
fof(f194_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n2),
inference(nnf_transformation,[status(thm)],[f194]) ).
fof(f194_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n2),
inference(skolemisation,[status(esa)],[f194_nnf]) ).
cnf(c263,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n2),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
fof(f195,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_176) ).
fof(f195_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n2),
inference(nnf_transformation,[status(thm)],[f195]) ).
fof(f195_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n2),
inference(skolemisation,[status(esa)],[f195_nnf]) ).
cnf(c264,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n2),
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
fof(f196,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_177) ).
fof(f196_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n2),
inference(nnf_transformation,[status(thm)],[f196]) ).
fof(f196_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n2),
inference(skolemisation,[status(esa)],[f196_nnf]) ).
cnf(c265,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n2),
inference(cnf_transformation,[status(esa)],[f196_sk]) ).
fof(f197,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_178) ).
fof(f197_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n3),
inference(nnf_transformation,[status(thm)],[f197]) ).
fof(f197_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n3),
inference(skolemisation,[status(esa)],[f197_nnf]) ).
cnf(c266,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n3),
inference(cnf_transformation,[status(esa)],[f197_sk]) ).
fof(f198,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_179) ).
fof(f198_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3),
inference(nnf_transformation,[status(thm)],[f198]) ).
fof(f198_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3),
inference(skolemisation,[status(esa)],[f198_nnf]) ).
cnf(c267,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3),
inference(cnf_transformation,[status(esa)],[f198_sk]) ).
fof(f199,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_180) ).
fof(f199_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n3),
inference(nnf_transformation,[status(thm)],[f199]) ).
fof(f199_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n3),
inference(skolemisation,[status(esa)],[f199_nnf]) ).
cnf(c268,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n3),
inference(cnf_transformation,[status(esa)],[f199_sk]) ).
fof(f200,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_181) ).
fof(f200_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n3),
inference(nnf_transformation,[status(thm)],[f200]) ).
fof(f200_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n3),
inference(skolemisation,[status(esa)],[f200_nnf]) ).
cnf(c269,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n3),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
fof(f201,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_182) ).
fof(f201_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n2),
inference(nnf_transformation,[status(thm)],[f201]) ).
fof(f201_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n2),
inference(skolemisation,[status(esa)],[f201_nnf]) ).
cnf(c270,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n2),
inference(cnf_transformation,[status(esa)],[f201_sk]) ).
fof(f203,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_184) ).
fof(f203_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n4),
inference(nnf_transformation,[status(thm)],[f203]) ).
fof(f203_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n4),
inference(skolemisation,[status(esa)],[f203_nnf]) ).
cnf(c272,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n4),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
fof(f204,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_185) ).
fof(f204_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n6),
inference(nnf_transformation,[status(thm)],[f204]) ).
fof(f204_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n6),
inference(skolemisation,[status(esa)],[f204_nnf]) ).
cnf(c273,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n6),
inference(cnf_transformation,[status(esa)],[f204_sk]) ).
fof(f205,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_186) ).
fof(f205_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n6),
inference(nnf_transformation,[status(thm)],[f205]) ).
fof(f205_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n6),
inference(skolemisation,[status(esa)],[f205_nnf]) ).
cnf(c274,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n6),
inference(cnf_transformation,[status(esa)],[f205_sk]) ).
fof(f206,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_187) ).
fof(f206_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6),
inference(nnf_transformation,[status(thm)],[f206]) ).
fof(f206_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6),
inference(skolemisation,[status(esa)],[f206_nnf]) ).
cnf(c275,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6),
inference(cnf_transformation,[status(esa)],[f206_sk]) ).
fof(f231,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_212) ).
fof(f231_nnf,plain,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n2),
inference(nnf_transformation,[status(thm)],[f231]) ).
fof(f231_sk,plain,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n2),
inference(skolemisation,[status(esa)],[f231_nnf]) ).
cnf(c300,plain,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n2),
inference(cnf_transformation,[status(esa)],[f231_sk]) ).
fof(f232,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_213) ).
fof(f232_nnf,plain,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n6),
inference(nnf_transformation,[status(thm)],[f232]) ).
fof(f232_sk,plain,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n6),
inference(skolemisation,[status(esa)],[f232_nnf]) ).
cnf(c301,plain,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n6),
inference(cnf_transformation,[status(esa)],[f232_sk]) ).
fof(f235,axiom,
~ accept_team(countryccivilorganization,countrybcivilorganization,towna,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_216) ).
fof(f235_nnf,plain,
~ accept_team(countryccivilorganization,countrybcivilorganization,towna,n6),
inference(nnf_transformation,[status(thm)],[f235]) ).
fof(f235_sk,plain,
~ accept_team(countryccivilorganization,countrybcivilorganization,towna,n6),
inference(skolemisation,[status(esa)],[f235_nnf]) ).
cnf(c304,plain,
~ accept_team(countryccivilorganization,countrybcivilorganization,towna,n6),
inference(cnf_transformation,[status(esa)],[f235_sk]) ).
fof(f236,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,towna,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_217) ).
fof(f236_nnf,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,towna,n6),
inference(nnf_transformation,[status(thm)],[f236]) ).
fof(f236_sk,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,towna,n6),
inference(skolemisation,[status(esa)],[f236_nnf]) ).
cnf(c305,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,towna,n6),
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
fof(f237,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,towna,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_218) ).
fof(f237_nnf,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,towna,n6),
inference(nnf_transformation,[status(thm)],[f237]) ).
fof(f237_sk,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,towna,n6),
inference(skolemisation,[status(esa)],[f237_nnf]) ).
cnf(c306,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,towna,n6),
inference(cnf_transformation,[status(esa)],[f237_sk]) ).
fof(f238,axiom,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_219) ).
fof(f238_nnf,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n6),
inference(nnf_transformation,[status(thm)],[f238]) ).
fof(f238_sk,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n6),
inference(skolemisation,[status(esa)],[f238_nnf]) ).
cnf(c307,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n6),
inference(cnf_transformation,[status(esa)],[f238_sk]) ).
fof(f265,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',event_246) ).
fof(f265_nnf,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n6),
inference(nnf_transformation,[status(thm)],[f265]) ).
fof(f265_sk,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n6),
inference(skolemisation,[status(esa)],[f265_nnf]) ).
cnf(c334,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n6),
inference(cnf_transformation,[status(esa)],[f265_sk]) ).
fof(f552,axiom,
! [X,Y] :
( less(X,Y)
<=> ( Y != X
& ~ less(Y,X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_property) ).
fof(f552_nnf,plain,
! [X,Y] :
( ( Y = X
| less(Y,X)
| less(X,Y) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f552]) ).
fof(f552_sk,plain,
! [X,Y] :
( ( Y = X
| less(Y,X)
| less(X,Y) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(skolemisation,[status(esa)],[f552_nnf]) ).
cnf(c621,plain,
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f552_sk]) ).
cnf(c622,plain,
( X1 != X0
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f552_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c9,c97,c98,c117,c118,c119,c120,c121,c122,c123,c124,c128,c159,c160,c203,c204,c205,c206,c207,c231,c232,c262,c263,c264,c265,c266,c267,c268,c269,c270,c272,c273,c274,c275,c300,c301,c304,c305,c306,c307,c334,c621,c622,c628]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t351]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : AGT005+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 04:22:52 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 13.21/2.31 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.21/2.31 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------