%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : AGT016+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.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:46 PM UTC 2026
% Result : Theorem 7.89s 1.57s
% Output : Proof 7.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 49
% Syntax : Number of formulae : 207 ( 194 unt; 0 def)
% Number of atoms : 261 ( 14 equ)
% Maximal formula atoms : 12 ( 1 avg)
% Number of connectives : 278 ( 224 ~; 31 |; 20 &)
% ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 33 ( 33 usr; 32 con; 0-4 aty)
% Number of variables : 39 ( 4 sgn 22 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [A] :
( ( accept_population(A,other,n0)
& accept_population(A,native,n0)
& accept_population(A,muslim,n1)
& accept_population(A,christian,n24)
& accept_population(A,atheist,n75) )
<=> accept_city(A,towna) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_9) ).
fof(f15_nnf,plain,
! [A] :
( ( ~ accept_city(A,towna)
| ( accept_population(A,other,n0)
& accept_population(A,native,n0)
& accept_population(A,muslim,n1)
& accept_population(A,christian,n24)
& accept_population(A,atheist,n75) ) )
& ( accept_city(A,towna)
| ~ accept_population(A,other,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,atheist,n75) ) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A] :
( ( ~ accept_city(A,towna)
| ( accept_population(A,other,n0)
& accept_population(A,native,n0)
& accept_population(A,muslim,n1)
& accept_population(A,christian,n24)
& accept_population(A,atheist,n75) ) )
& ( accept_city(A,towna)
| ~ accept_population(A,other,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,atheist,n75) ) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c59,plain,
( accept_city(X0,towna)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(hi58,axiom,
ifeq(accept_population(X0,atheist,n75),true,ifeq(accept_population(X0,christian,n24),true,ifeq(accept_population(X0,muslim,n1),true,ifeq(accept_population(X0,native,n0),true,ifeq(accept_population(X0,other,n0),true,accept_city(X0,towna),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c59]) ).
fof(f922,conjecture,
? [X,Y] : ~ accept_population(muslimcountrybhumanitarianorganization,X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query_16) ).
fof(f922_neg,negated_conjecture,
~ ? [X,Y] : ~ accept_population(muslimcountrybhumanitarianorganization,X,Y),
inference(negated_conjecture,[status(cth)],[f922]) ).
fof(f922_nnf,plain,
! [X,Y] : accept_population(muslimcountrybhumanitarianorganization,X,Y),
inference(nnf_transformation,[status(thm)],[f922_neg]) ).
fof(f922_sk,plain,
! [X,Y] : accept_population(muslimcountrybhumanitarianorganization,X,Y),
inference(skolemisation,[status(esa)],[f922_nnf]) ).
cnf(c995,plain,
accept_population(muslimcountrybhumanitarianorganization,X0,X1),
inference(cnf_transformation,[status(esa)],[f922_sk]) ).
cnf(hi947,negated_conjecture,
accept_population(muslimcountrybhumanitarianorganization,X0,X1) = true,
inference(equality_encoding,[status(esa)],[c995]) ).
cnf(h2432,plain,
accept_city(muslimcountrybhumanitarianorganization,towna) = true,
inference(hyper_resolution,[status(thm)],[hi58,hi947,hi947,hi947,hi947,hi947]) ).
fof(f634,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,towna),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_366) ).
fof(f634_nnf,plain,
~ accept_city(muslimcountrybhumanitarianorganization,towna),
inference(nnf_transformation,[status(thm)],[f634]) ).
fof(f634_sk,plain,
~ accept_city(muslimcountrybhumanitarianorganization,towna),
inference(skolemisation,[status(esa)],[f634_nnf]) ).
cnf(c703,plain,
~ accept_city(muslimcountrybhumanitarianorganization,towna),
inference(cnf_transformation,[status(esa)],[f634_sk]) ).
cnf(hi993,axiom,
ifeq(accept_city(muslimcountrybhumanitarianorganization,towna),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c703]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi993,h2432]) ).
cnf(t57,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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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(f281,axiom,
~ accept_city(countryamedicalorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_13) ).
fof(f281_nnf,plain,
~ accept_city(countryamedicalorganization,coastvillage),
inference(nnf_transformation,[status(thm)],[f281]) ).
fof(f281_sk,plain,
~ accept_city(countryamedicalorganization,coastvillage),
inference(skolemisation,[status(esa)],[f281_nnf]) ).
cnf(c350,plain,
~ accept_city(countryamedicalorganization,coastvillage),
inference(cnf_transformation,[status(esa)],[f281_sk]) ).
fof(f326,axiom,
~ accept_number(countryccivilorganization,n5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_58) ).
fof(f326_nnf,plain,
~ accept_number(countryccivilorganization,n5),
inference(nnf_transformation,[status(thm)],[f326]) ).
fof(f326_sk,plain,
~ accept_number(countryccivilorganization,n5),
inference(skolemisation,[status(esa)],[f326_nnf]) ).
cnf(c395,plain,
~ accept_number(countryccivilorganization,n5),
inference(cnf_transformation,[status(esa)],[f326_sk]) ).
fof(f330,axiom,
~ accept_number(countryccivilorganization,n6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_62) ).
fof(f330_nnf,plain,
~ accept_number(countryccivilorganization,n6),
inference(nnf_transformation,[status(thm)],[f330]) ).
fof(f330_sk,plain,
~ accept_number(countryccivilorganization,n6),
inference(skolemisation,[status(esa)],[f330_nnf]) ).
cnf(c399,plain,
~ accept_number(countryccivilorganization,n6),
inference(cnf_transformation,[status(esa)],[f330_sk]) ).
fof(f350,axiom,
~ accept_leader(christiansufferterrahumanitarianorganization,sufferterragovernment),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_82) ).
fof(f350_nnf,plain,
~ accept_leader(christiansufferterrahumanitarianorganization,sufferterragovernment),
inference(nnf_transformation,[status(thm)],[f350]) ).
fof(f350_sk,plain,
~ accept_leader(christiansufferterrahumanitarianorganization,sufferterragovernment),
inference(skolemisation,[status(esa)],[f350_nnf]) ).
cnf(c419,plain,
~ accept_leader(christiansufferterrahumanitarianorganization,sufferterragovernment),
inference(cnf_transformation,[status(esa)],[f350_sk]) ).
fof(f919,axiom,
! [X,Y] :
( less(X,Y)
<=> ( Y != X
& ~ less(Y,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_property) ).
fof(f919_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)],[f919]) ).
fof(f919_sk,plain,
! [X,Y] :
( ( Y = X
| less(Y,X)
| less(X,Y) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(skolemisation,[status(esa)],[f919_nnf]) ).
cnf(c988,plain,
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f919_sk]) ).
cnf(c989,plain,
( X1 != X0
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f919_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,c350,c395,c399,c419,c703,c988,c989]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t57]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : AGT016+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n014.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:24:47 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.89/1.57 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.89/1.57 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------