%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO578+1 : TPTP v9.3.1. Released v5.5.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 : n012.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 09:12:06 AM UTC 2026
% Result : Theorem 30.08s 30.49s
% Output : Proof 30.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 2
% Syntax : Number of formulae : 34 ( 12 unt; 0 def)
% Number of atoms : 200 ( 0 equ)
% Maximal formula atoms : 22 ( 5 avg)
% Number of connectives : 258 ( 92 ~; 87 |; 72 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 3 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 73 ( 0 sgn 46 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos_21,axiom,
( ? [X62] :
( ~ k04_buttercup10100(X62)
& b48_buttercup10098(X62) )
& ! [X61] :
( k04_buttercup10100(X61)
=> b48_buttercup10098(X61) ) ),
file('theBenchmark.p',sos_21) ).
fof(goals_86,conjecture,
( ! [X149] :
( k04_buttercup10100(X149)
=> ~ b48_buttercup10098(X149) )
| ? [X146,X147,X148] :
( b48_buttercup10098(X148)
& ~ k04_buttercup10100(X148)
& ~ b48_buttercup10098(X147)
& k04_buttercup10100(X147)
& b48_buttercup10098(X146)
& k04_buttercup10100(X146) )
| ( ? [X145] :
( ~ k04_buttercup10100(X145)
& b48_buttercup10098(X145) )
& ! [X144] :
( k04_buttercup10100(X144)
=> b48_buttercup10098(X144) ) )
| ( ? [X143] :
( ~ b48_buttercup10098(X143)
& k04_buttercup10100(X143) )
& ! [X142] :
( b48_buttercup10098(X142)
=> k04_buttercup10100(X142) ) ) ),
file('theBenchmark.p',goals_86) ).
fof(f_21_1,plain,
( ? [X62] :
( ~ k04_buttercup10100(X62)
& b48_buttercup10098(X62) )
& ! [X61] :
( b48_buttercup10098(X61)
| ~ k04_buttercup10100(X61) ) ),
inference(fof_nnf,[status(thm)],[sos_21]) ).
fof(f_21_2,plain,
( ? [U_62] :
( ~ k04_buttercup10100(U_62)
& b48_buttercup10098(U_62) )
& ! [U_61] :
( b48_buttercup10098(U_61)
| ~ k04_buttercup10100(U_61) ) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
fof(f_21_3,plain,
( ~ k04_buttercup10100(sK32)
& b48_buttercup10098(sK32)
& ! [U_61] :
( b48_buttercup10098(U_61)
| ~ k04_buttercup10100(U_61) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(U_62,sK32)],[f_21_2]) ).
fof(f_21_4,plain,
( ~ k04_buttercup10100(sK32)
& b48_buttercup10098(sK32)
& ! [U_61] :
( b48_buttercup10098(U_61)
| ~ k04_buttercup10100(U_61) ) ),
inference(definitional_conversion,[status(esa)],[f_21_3]) ).
cnf(f_21_5,plain,
( b48_buttercup10098(U_61)
| ~ k04_buttercup10100(U_61) ),
inference(clausify,[status(thm)],[f_21_4]) ).
cnf(f_21_6,plain,
b48_buttercup10098(sK32),
inference(clausify,[status(thm)],[f_21_4]) ).
cnf(f_21_7,plain,
~ k04_buttercup10100(sK32),
inference(clausify,[status(thm)],[f_21_4]) ).
fof(f_86_1,negated_conjecture,
~ ( ! [X149] :
( k04_buttercup10100(X149)
=> ~ b48_buttercup10098(X149) )
| ? [X146,X147,X148] :
( b48_buttercup10098(X148)
& ~ k04_buttercup10100(X148)
& ~ b48_buttercup10098(X147)
& k04_buttercup10100(X147)
& b48_buttercup10098(X146)
& k04_buttercup10100(X146) )
| ( ? [X145] :
( ~ k04_buttercup10100(X145)
& b48_buttercup10098(X145) )
& ! [X144] :
( k04_buttercup10100(X144)
=> b48_buttercup10098(X144) ) )
| ( ? [X143] :
( ~ b48_buttercup10098(X143)
& k04_buttercup10100(X143) )
& ! [X142] :
( b48_buttercup10098(X142)
=> k04_buttercup10100(X142) ) ) ),
inference(negate,[status(cth)],[goals_86]) ).
fof(f_86_2,negated_conjecture,
( ? [X149] :
( b48_buttercup10098(X149)
& k04_buttercup10100(X149) )
& ! [X146,X147,X148] :
( ~ b48_buttercup10098(X148)
| k04_buttercup10100(X148)
| b48_buttercup10098(X147)
| ~ k04_buttercup10100(X147)
| ~ b48_buttercup10098(X146)
| ~ k04_buttercup10100(X146) )
& ( ! [X145] :
( k04_buttercup10100(X145)
| ~ b48_buttercup10098(X145) )
| ? [X144] :
( ~ b48_buttercup10098(X144)
& k04_buttercup10100(X144) ) )
& ( ! [X143] :
( b48_buttercup10098(X143)
| ~ k04_buttercup10100(X143) )
| ? [X142] :
( ~ k04_buttercup10100(X142)
& b48_buttercup10098(X142) ) ) ),
inference(fof_nnf,[status(thm)],[f_86_1]) ).
fof(f_86_3,negated_conjecture,
( ? [U_151] :
( b48_buttercup10098(U_151)
& k04_buttercup10100(U_151) )
& ! [U_150,U_149,U_148] :
( ~ b48_buttercup10098(U_148)
| k04_buttercup10100(U_148)
| b48_buttercup10098(U_149)
| ~ k04_buttercup10100(U_149)
| ~ b48_buttercup10098(U_150)
| ~ k04_buttercup10100(U_150) )
& ( ! [U_147] :
( k04_buttercup10100(U_147)
| ~ b48_buttercup10098(U_147) )
| ? [U_146] :
( ~ b48_buttercup10098(U_146)
& k04_buttercup10100(U_146) ) )
& ( ! [U_145] :
( b48_buttercup10098(U_145)
| ~ k04_buttercup10100(U_145) )
| ? [U_144] :
( ~ k04_buttercup10100(U_144)
& b48_buttercup10098(U_144) ) ) ),
inference(variable_rename,[status(thm)],[f_86_2]) ).
fof(f_86_4,negated_conjecture,
( ? [U_151] :
( b48_buttercup10098(U_151)
& k04_buttercup10100(U_151) )
& ( ! [U_150] :
( ~ b48_buttercup10098(U_150)
| ~ k04_buttercup10100(U_150) )
| ! [U_149] :
( b48_buttercup10098(U_149)
| ~ k04_buttercup10100(U_149) )
| ! [U_148] :
( ~ b48_buttercup10098(U_148)
| k04_buttercup10100(U_148) ) )
& ( ! [U_147] :
( k04_buttercup10100(U_147)
| ~ b48_buttercup10098(U_147) )
| ? [U_146] :
( ~ b48_buttercup10098(U_146)
& k04_buttercup10100(U_146) ) )
& ( ! [U_145] :
( b48_buttercup10098(U_145)
| ~ k04_buttercup10100(U_145) )
| ? [U_144] :
( ~ k04_buttercup10100(U_144)
& b48_buttercup10098(U_144) ) ) ),
inference(miniscope,[status(thm)],[f_86_3]) ).
fof(f_86_5,negated_conjecture,
( ? [U_151] :
( b48_buttercup10098(U_151)
& k04_buttercup10100(U_151) )
& ( ! [U_150] :
( ~ b48_buttercup10098(U_150)
| ~ k04_buttercup10100(U_150) )
| ! [U_149] :
( b48_buttercup10098(U_149)
| ~ k04_buttercup10100(U_149) )
| ! [U_148] :
( ~ b48_buttercup10098(U_148)
| k04_buttercup10100(U_148) ) )
& ( ! [U_147] :
( k04_buttercup10100(U_147)
| ~ b48_buttercup10098(U_147) )
| ? [U_146] :
( ~ b48_buttercup10098(U_146)
& k04_buttercup10100(U_146) ) )
& ( ! [U_145] :
( b48_buttercup10098(U_145)
| ~ k04_buttercup10100(U_145) )
| ( ~ k04_buttercup10100(sK56)
& b48_buttercup10098(sK56) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56]),skolemize(U_144,sK56)],[f_86_4]) ).
fof(f_86_6,negated_conjecture,
( ? [U_151] :
( b48_buttercup10098(U_151)
& k04_buttercup10100(U_151) )
& ( ! [U_150] :
( ~ b48_buttercup10098(U_150)
| ~ k04_buttercup10100(U_150) )
| ! [U_149] :
( b48_buttercup10098(U_149)
| ~ k04_buttercup10100(U_149) )
| ! [U_148] :
( ~ b48_buttercup10098(U_148)
| k04_buttercup10100(U_148) ) )
& ( ! [U_147] :
( k04_buttercup10100(U_147)
| ~ b48_buttercup10098(U_147) )
| ( ~ b48_buttercup10098(sK57)
& k04_buttercup10100(sK57) ) )
& ( ! [U_145] :
( b48_buttercup10098(U_145)
| ~ k04_buttercup10100(U_145) )
| ( ~ k04_buttercup10100(sK56)
& b48_buttercup10098(sK56) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57]),skolemize(U_146,sK57)],[f_86_5]) ).
fof(f_86_7,negated_conjecture,
( b48_buttercup10098(sK58)
& k04_buttercup10100(sK58)
& ( ! [U_150] :
( ~ b48_buttercup10098(U_150)
| ~ k04_buttercup10100(U_150) )
| ! [U_149] :
( b48_buttercup10098(U_149)
| ~ k04_buttercup10100(U_149) )
| ! [U_148] :
( ~ b48_buttercup10098(U_148)
| k04_buttercup10100(U_148) ) )
& ( ! [U_147] :
( k04_buttercup10100(U_147)
| ~ b48_buttercup10098(U_147) )
| ( ~ b48_buttercup10098(sK57)
& k04_buttercup10100(sK57) ) )
& ( ! [U_145] :
( b48_buttercup10098(U_145)
| ~ k04_buttercup10100(U_145) )
| ( ~ k04_buttercup10100(sK56)
& b48_buttercup10098(sK56) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58]),skolemize(U_151,sK58)],[f_86_6]) ).
fof(f_86_8,negated_conjecture,
( ( ~ b48_buttercup10098(sK57)
| ~ sP22 )
& ( k04_buttercup10100(sK57)
| ~ sP22 )
& ( ~ k04_buttercup10100(sK56)
| ~ sP21 )
& ( b48_buttercup10098(sK56)
| ~ sP21 )
& b48_buttercup10098(sK58)
& k04_buttercup10100(sK58)
& ! [U_148,U_149,U_150] :
( ~ b48_buttercup10098(U_150)
| ~ k04_buttercup10100(U_150)
| b48_buttercup10098(U_149)
| ~ k04_buttercup10100(U_149)
| ~ b48_buttercup10098(U_148)
| k04_buttercup10100(U_148) )
& ! [U_147] :
( k04_buttercup10100(U_147)
| ~ b48_buttercup10098(U_147)
| sP22 )
& ! [U_145] :
( b48_buttercup10098(U_145)
| ~ k04_buttercup10100(U_145)
| sP21 ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP21,sP22])],[f_86_7]) ).
cnf(f_86_10,negated_conjecture,
( k04_buttercup10100(U_147)
| ~ b48_buttercup10098(U_147)
| sP22 ),
inference(clausify,[status(thm)],[f_86_8]) ).
cnf(f_86_16,negated_conjecture,
( k04_buttercup10100(sK57)
| ~ sP22 ),
inference(clausify,[status(thm)],[f_86_8]) ).
cnf(f_86_17,negated_conjecture,
( ~ b48_buttercup10098(sK57)
| ~ sP22 ),
inference(clausify,[status(thm)],[f_86_8]) ).
cnf(t1,plain,
( k04_buttercup10100(sK57)
| ~ sP22 ),
inference(start,[status(thm),parent(0:0)],[f_86_16]) ).
cnf(t2,plain,
( ~ b48_buttercup10098(sK32)
| k04_buttercup10100(sK32)
| sP22 ),
inference(extension,[status(thm),parent(t1:1)],[f_86_10]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
~ k04_buttercup10100(sK32),
inference(extension,[status(thm),parent(t2:2)],[f_21_7]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
b48_buttercup10098(sK32),
inference(extension,[status(thm),parent(t2:3)],[f_21_6]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t2:3]) ).
cnf(l1,lemma,
sP22,
inference(lemma,[status(cth),parent(t1:1),below(0:0)],[t1:1]) ).
cnf(t8,plain,
( b48_buttercup10098(sK57)
| ~ k04_buttercup10100(sK57) ),
inference(extension,[status(thm),parent(t1:2)],[f_21_5]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t1:2]) ).
cnf(t10,plain,
( ~ sP22
| ~ b48_buttercup10098(sK57) ),
inference(extension,[status(thm),parent(t8:2)],[f_86_17]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
sP22,
inference(lemma_extension,[status(thm),parent(t10:2)],[l1:1]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYO578+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.02 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.02 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.02/0.36 % Computer : n012.cluster.edu
% 0.02/0.36 % Model : x86_64 x86_64
% 0.02/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.36 % Memory : 8046.5625MB
% 0.02/0.36 % OS : Linux 6.8.0-71-generic
% 0.02/0.36 % CPULimit : 300
% 0.02/0.36 % WCLimit : 300
% 0.02/0.36 % DateTime : Sun Sep 20 07:41:22 UTC 2026
% 0.02/0.36 % CPUTime :
% 30.08/30.49 % SZS status Theorem for theBenchmark
% 30.08/30.49 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------