%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NLP258-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 : Thu Sep 24 08:51:34 AM UTC 2026
% Result : Unsatisfiable 222.00s 222.36s
% Output : Proof 222.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,axiom,
( event(U,V)
| ~ smoke(U,V) ),
file('theBenchmark.p',clause1) ).
cnf(clause2,axiom,
( eventuality(U,V)
| ~ event(U,V) ),
file('theBenchmark.p',clause2) ).
cnf(clause3,axiom,
( thing(U,V)
| ~ eventuality(U,V) ),
file('theBenchmark.p',clause3) ).
cnf(clause4,axiom,
( singleton(U,V)
| ~ thing(U,V) ),
file('theBenchmark.p',clause4) ).
cnf(clause5,axiom,
( specific(U,V)
| ~ eventuality(U,V) ),
file('theBenchmark.p',clause5) ).
cnf(clause6,axiom,
( nonexistent(U,V)
| ~ eventuality(U,V) ),
file('theBenchmark.p',clause6) ).
cnf(clause7,axiom,
( unisex(U,V)
| ~ eventuality(U,V) ),
file('theBenchmark.p',clause7) ).
cnf(clause8,axiom,
( relation(U,V)
| ~ proposition(U,V) ),
file('theBenchmark.p',clause8) ).
cnf(clause9,axiom,
( abstraction(U,V)
| ~ relation(U,V) ),
file('theBenchmark.p',clause9) ).
cnf(clause10,axiom,
( thing(U,V)
| ~ abstraction(U,V) ),
file('theBenchmark.p',clause10) ).
cnf(clause11,axiom,
( nonhuman(U,V)
| ~ abstraction(U,V) ),
file('theBenchmark.p',clause11) ).
cnf(clause12,axiom,
( general(U,V)
| ~ abstraction(U,V) ),
file('theBenchmark.p',clause12) ).
cnf(clause13,axiom,
( unisex(U,V)
| ~ abstraction(U,V) ),
file('theBenchmark.p',clause13) ).
cnf(clause14,axiom,
( eventuality(U,V)
| ~ state(U,V) ),
file('theBenchmark.p',clause14) ).
cnf(clause15,axiom,
( event(U,V)
| ~ state(U,V) ),
file('theBenchmark.p',clause15) ).
cnf(clause16,axiom,
( human_person(U,V)
| ~ man(U,V) ),
file('theBenchmark.p',clause16) ).
cnf(clause17,axiom,
( organism(U,V)
| ~ human_person(U,V) ),
file('theBenchmark.p',clause17) ).
cnf(clause18,axiom,
( entity(U,V)
| ~ organism(U,V) ),
file('theBenchmark.p',clause18) ).
cnf(clause19,axiom,
( thing(U,V)
| ~ entity(U,V) ),
file('theBenchmark.p',clause19) ).
cnf(clause20,axiom,
( specific(U,V)
| ~ entity(U,V) ),
file('theBenchmark.p',clause20) ).
cnf(clause21,axiom,
( existent(U,V)
| ~ entity(U,V) ),
file('theBenchmark.p',clause21) ).
cnf(clause22,axiom,
( impartial(U,V)
| ~ organism(U,V) ),
file('theBenchmark.p',clause22) ).
cnf(clause23,axiom,
( living(U,V)
| ~ organism(U,V) ),
file('theBenchmark.p',clause23) ).
cnf(clause24,axiom,
( human(U,V)
| ~ human_person(U,V) ),
file('theBenchmark.p',clause24) ).
cnf(clause25,axiom,
( animate(U,V)
| ~ human_person(U,V) ),
file('theBenchmark.p',clause25) ).
cnf(clause26,axiom,
( male(U,V)
| ~ man(U,V) ),
file('theBenchmark.p',clause26) ).
cnf(clause27,axiom,
( relname(U,V)
| ~ forename(U,V) ),
file('theBenchmark.p',clause27) ).
cnf(clause28,axiom,
( relation(U,V)
| ~ relname(U,V) ),
file('theBenchmark.p',clause28) ).
cnf(clause29,axiom,
( forename(U,V)
| ~ vincent_forename(U,V) ),
file('theBenchmark.p',clause29) ).
cnf(clause30,axiom,
( forename(U,V)
| ~ jules_forename(U,V) ),
file('theBenchmark.p',clause30) ).
cnf(clause31,axiom,
( ~ unisex(U,V)
| ~ male(U,V) ),
file('theBenchmark.p',clause31) ).
cnf(clause32,axiom,
( ~ specific(U,V)
| ~ general(U,V) ),
file('theBenchmark.p',clause32) ).
cnf(clause33,axiom,
( ~ nonhuman(U,V)
| ~ human(U,V) ),
file('theBenchmark.p',clause33) ).
cnf(clause34,axiom,
( ~ existent(U,V)
| ~ nonexistent(U,V) ),
file('theBenchmark.p',clause34) ).
cnf(clause35,axiom,
( W = X
| ~ be(U,V,W,X) ),
file('theBenchmark.p',clause35) ).
cnf(clause36,axiom,
( smoke(V,W)
| ~ smoke(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause36) ).
cnf(clause37,axiom,
( event(V,W)
| ~ event(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause37) ).
cnf(clause38,axiom,
( eventuality(V,W)
| ~ eventuality(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause38) ).
cnf(clause39,axiom,
( thing(V,W)
| ~ thing(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause39) ).
cnf(clause40,axiom,
( singleton(V,W)
| ~ singleton(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause40) ).
cnf(clause41,axiom,
( specific(V,W)
| ~ specific(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause41) ).
cnf(clause42,axiom,
( nonexistent(V,W)
| ~ nonexistent(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause42) ).
cnf(clause43,axiom,
( unisex(V,W)
| ~ unisex(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause43) ).
cnf(clause44,axiom,
( present(V,W)
| ~ present(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause44) ).
cnf(clause45,axiom,
( think_believe_consider(V,W)
| ~ think_believe_consider(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause45) ).
cnf(clause46,axiom,
( proposition(V,W)
| ~ proposition(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause46) ).
cnf(clause47,axiom,
( relation(V,W)
| ~ relation(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause47) ).
cnf(clause48,axiom,
( abstraction(V,W)
| ~ abstraction(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause48) ).
cnf(clause49,axiom,
( nonhuman(V,W)
| ~ nonhuman(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause49) ).
cnf(clause50,axiom,
( general(V,W)
| ~ general(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause50) ).
cnf(clause51,axiom,
( state(V,W)
| ~ state(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause51) ).
cnf(clause52,axiom,
( man(V,W)
| ~ man(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause52) ).
cnf(clause53,axiom,
( human_person(V,W)
| ~ human_person(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause53) ).
cnf(clause54,axiom,
( organism(V,W)
| ~ organism(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause54) ).
cnf(clause55,axiom,
( entity(V,W)
| ~ entity(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause55) ).
cnf(clause56,axiom,
( existent(V,W)
| ~ existent(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause56) ).
cnf(clause57,axiom,
( impartial(V,W)
| ~ impartial(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause57) ).
cnf(clause58,axiom,
( living(V,W)
| ~ living(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause58) ).
cnf(clause59,axiom,
( human(V,W)
| ~ human(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause59) ).
cnf(clause60,axiom,
( animate(V,W)
| ~ animate(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause60) ).
cnf(clause61,axiom,
( male(V,W)
| ~ male(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause61) ).
cnf(clause62,axiom,
( forename(V,W)
| ~ forename(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause62) ).
cnf(clause63,axiom,
( relname(V,W)
| ~ relname(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause63) ).
cnf(clause64,axiom,
( vincent_forename(V,W)
| ~ vincent_forename(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause64) ).
cnf(clause65,axiom,
( jules_forename(V,W)
| ~ jules_forename(U,W)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause65) ).
cnf(clause66,axiom,
( agent(V,W,X)
| ~ agent(U,W,X)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause66) ).
cnf(clause67,axiom,
( theme(V,W,X)
| ~ theme(U,W,X)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause67) ).
cnf(clause68,axiom,
( of(V,W,X)
| ~ of(U,W,X)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause68) ).
cnf(clause69,axiom,
( be(V,W,X,Y)
| ~ be(U,W,X,Y)
| ~ accessible_world(U,V) ),
file('theBenchmark.p',clause69) ).
cnf(clause70,axiom,
( W = V
| ~ entity(U,X)
| ~ of(U,V,X)
| ~ forename(U,W)
| ~ of(U,W,X)
| ~ forename(U,V) ),
file('theBenchmark.p',clause70) ).
cnf(clause71,axiom,
( V = W
| ~ agent(U,X,Z)
| ~ agent(U,Y,Z)
| ~ theme(U,Y,W)
| ~ think_believe_consider(U,Y)
| ~ think_believe_consider(U,X)
| ~ theme(U,X,V)
| ~ proposition(U,W)
| ~ proposition(U,V) ),
file('theBenchmark.p',clause71) ).
cnf(clause72,negated_conjecture,
actual_world(skc8),
file('theBenchmark.p',clause72) ).
cnf(clause73,negated_conjecture,
man(skc8,skc15),
file('theBenchmark.p',clause73) ).
cnf(clause74,negated_conjecture,
forename(skc8,skc14),
file('theBenchmark.p',clause74) ).
cnf(clause75,negated_conjecture,
vincent_forename(skc8,skc14),
file('theBenchmark.p',clause75) ).
cnf(clause76,negated_conjecture,
event(skc8,skc13),
file('theBenchmark.p',clause76) ).
cnf(clause77,negated_conjecture,
present(skc8,skc13),
file('theBenchmark.p',clause77) ).
cnf(clause78,negated_conjecture,
think_believe_consider(skc8,skc13),
file('theBenchmark.p',clause78) ).
cnf(clause79,negated_conjecture,
jules_forename(skc8,skc11),
file('theBenchmark.p',clause79) ).
cnf(clause80,negated_conjecture,
forename(skc8,skc11),
file('theBenchmark.p',clause80) ).
cnf(clause81,negated_conjecture,
man(skc8,skc10),
file('theBenchmark.p',clause81) ).
cnf(clause82,negated_conjecture,
state(skc8,skc9),
file('theBenchmark.p',clause82) ).
cnf(clause83,negated_conjecture,
accessible_world(skc8,skc12),
file('theBenchmark.p',clause83) ).
cnf(clause84,negated_conjecture,
proposition(skc8,skc12),
file('theBenchmark.p',clause84) ).
cnf(clause85,negated_conjecture,
of(skc8,skc14,skc15),
file('theBenchmark.p',clause85) ).
cnf(clause86,negated_conjecture,
agent(skc8,skc13,skc15),
file('theBenchmark.p',clause86) ).
cnf(clause87,negated_conjecture,
theme(skc8,skc13,skc12),
file('theBenchmark.p',clause87) ).
cnf(clause88,negated_conjecture,
of(skc8,skc11,skc10),
file('theBenchmark.p',clause88) ).
cnf(clause89,negated_conjecture,
be(skc8,skc9,skc10,skc10),
file('theBenchmark.p',clause89) ).
cnf(clause90,negated_conjecture,
( smoke(skc12,skf2(V))
| ~ man(skc12,U) ),
file('theBenchmark.p',clause90) ).
cnf(clause91,negated_conjecture,
( present(skc12,skf2(V))
| ~ man(skc12,U) ),
file('theBenchmark.p',clause91) ).
cnf(clause92,negated_conjecture,
( event(skc12,skf2(V))
| ~ man(skc12,U) ),
file('theBenchmark.p',clause92) ).
cnf(clause93,negated_conjecture,
( agent(skc12,skf2(U),U)
| ~ man(skc12,U) ),
file('theBenchmark.p',clause93) ).
cnf(clause94,negated_conjecture,
( man(X1,skf4(X1))
| ~ actual_world(U)
| ~ think_believe_consider(U,X3)
| ~ present(U,X3)
| ~ event(U,X3)
| ~ theme(U,X3,X)
| ~ forename(U,X5)
| ~ vincent_forename(U,X5)
| ~ of(U,X5,X4)
| ~ man(U,X4)
| ~ agent(U,X2,X4)
| ~ agent(U,X3,X4)
| ~ theme(U,X2,X1)
| ~ event(U,X2)
| ~ present(U,X2)
| ~ think_believe_consider(U,X2)
| ~ accessible_world(U,X1)
| ~ proposition(U,X1)
| ~ proposition(U,X)
| ~ accessible_world(U,X)
| ~ of(U,Z,W)
| ~ jules_forename(U,Z)
| ~ forename(U,Z)
| ~ event(X,Y)
| ~ agent(X,Y,W)
| ~ present(X,Y)
| ~ smoke(X,Y)
| ~ be(U,V,W,W)
| ~ man(U,W)
| ~ state(U,V) ),
file('theBenchmark.p',clause94) ).
cnf(clause95,negated_conjecture,
( ~ actual_world(U)
| ~ think_believe_consider(U,X4)
| ~ present(U,X4)
| ~ event(U,X4)
| ~ theme(U,X4,X)
| ~ forename(U,X6)
| ~ vincent_forename(U,X6)
| ~ of(U,X6,X5)
| ~ man(U,X5)
| ~ agent(U,X3,X5)
| ~ agent(U,X4,X5)
| ~ theme(U,X3,X1)
| ~ event(U,X3)
| ~ present(U,X3)
| ~ think_believe_consider(U,X3)
| ~ event(X1,X2)
| ~ agent(X1,X2,skf4(X1))
| ~ present(X1,X2)
| ~ smoke(X1,X2)
| ~ accessible_world(U,X1)
| ~ proposition(U,X1)
| ~ proposition(U,X)
| ~ accessible_world(U,X)
| ~ of(U,Z,W)
| ~ jules_forename(U,Z)
| ~ forename(U,Z)
| ~ event(X,Y)
| ~ agent(X,Y,W)
| ~ present(X,Y)
| ~ smoke(X,Y)
| ~ be(U,V,W,W)
| ~ man(U,W)
| ~ state(U,V) ),
file('theBenchmark.p',clause95) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( skf2(Eq_x_0) = skf2(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( skf4(Eq_x_0) = skf4(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( smoke(Eq_y_0,Eq_y_1)
| ~ smoke(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_7,axiom,
( event(Eq_y_0,Eq_y_1)
| ~ event(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_8,axiom,
( eventuality(Eq_y_0,Eq_y_1)
| ~ eventuality(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_9,axiom,
( thing(Eq_y_0,Eq_y_1)
| ~ thing(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_10,axiom,
( singleton(Eq_y_0,Eq_y_1)
| ~ singleton(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_11,axiom,
( specific(Eq_y_0,Eq_y_1)
| ~ specific(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,axiom,
( nonexistent(Eq_y_0,Eq_y_1)
| ~ nonexistent(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( unisex(Eq_y_0,Eq_y_1)
| ~ unisex(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( proposition(Eq_y_0,Eq_y_1)
| ~ proposition(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( relation(Eq_y_0,Eq_y_1)
| ~ relation(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( abstraction(Eq_y_0,Eq_y_1)
| ~ abstraction(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( nonhuman(Eq_y_0,Eq_y_1)
| ~ nonhuman(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( general(Eq_y_0,Eq_y_1)
| ~ general(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( state(Eq_y_0,Eq_y_1)
| ~ state(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_20,axiom,
( man(Eq_y_0,Eq_y_1)
| ~ man(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( human_person(Eq_y_0,Eq_y_1)
| ~ human_person(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_22,axiom,
( organism(Eq_y_0,Eq_y_1)
| ~ organism(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_23,axiom,
( entity(Eq_y_0,Eq_y_1)
| ~ entity(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_24,axiom,
( existent(Eq_y_0,Eq_y_1)
| ~ existent(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_25,axiom,
( impartial(Eq_y_0,Eq_y_1)
| ~ impartial(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_26,axiom,
( living(Eq_y_0,Eq_y_1)
| ~ living(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_27,axiom,
( human(Eq_y_0,Eq_y_1)
| ~ human(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_28,axiom,
( animate(Eq_y_0,Eq_y_1)
| ~ animate(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_29,axiom,
( male(Eq_y_0,Eq_y_1)
| ~ male(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_30,axiom,
( forename(Eq_y_0,Eq_y_1)
| ~ forename(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_31,axiom,
( relname(Eq_y_0,Eq_y_1)
| ~ relname(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_32,axiom,
( vincent_forename(Eq_y_0,Eq_y_1)
| ~ vincent_forename(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_33,axiom,
( jules_forename(Eq_y_0,Eq_y_1)
| ~ jules_forename(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_34,axiom,
( be(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ be(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_35,axiom,
( accessible_world(Eq_y_0,Eq_y_1)
| ~ accessible_world(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_36,axiom,
( present(Eq_y_0,Eq_y_1)
| ~ present(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_37,axiom,
( think_believe_consider(Eq_y_0,Eq_y_1)
| ~ think_believe_consider(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_38,axiom,
( agent(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ agent(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_39,axiom,
( theme(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ theme(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_40,axiom,
( of(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ of(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_41,axiom,
( actual_world(Eq_y_0)
| ~ actual_world(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP258-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a CNF_UNS_RFO_SEQ_HRN problem
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n002.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 19 17:34:50 UTC 2026
% 0.09/0.35 % CPUTime :
% 222.00/222.36 % SZS status Unsatisfiable for theBenchmark
% 222.00/222.36 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------