%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1.1
% Problem : MGT041+2 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 : Tue Sep 8 06:20:10 AM UTC 2026
% Result : Theorem 0.09s 0.37s
% Output : Proof 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 5
% Syntax : Number of formulae : 26 ( 5 unt; 0 def)
% Number of atoms : 76 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 83 ( 33 ~; 18 |; 28 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 40 ( 1 sgn 20 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
% FILE RECORD
fof(a15,hypothesis,
! [X1,X2] :
( ( organisation_at_time(X1,X2)
& first_mover(X1)
& founding_time(X1,X2) )
=> number_of_routines(X1,X2,low) ),
file('theBenchmark.p',a15) ).
% FOF SIMPLE INFERENCE
fof(a15_elimTB,hypothesis,
! [X1,X2] :
( ( organisation_at_time(X1,X2)
& first_mover(X1)
& founding_time(X1,X2) )
=> number_of_routines(X1,X2,low) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[a15])]) ).
% FOF SIMPLE INFERENCE
fof(a15_elimImpEquivPushNegMiniScope,hypothesis,
! [X1,X2] :
( ~ organisation_at_time(X1,X2)
| ~ first_mover(X1)
| ~ founding_time(X1,X2)
| number_of_routines(X1,X2,low) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[a15_elimTB]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_3,plain,
( ~ organisation_at_time(X0,X1)
| ~ first_mover(X0)
| ~ founding_time(X0,X1)
| number_of_routines(X0,X1,low) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[a15_elimImpEquivPushNegMiniScope])]) ).
% FILE RECORD
fof(mp_not_high_and_low,axiom,
! [X1,X2] :
~ ( number_of_routines(X1,X2,low)
& number_of_routines(X1,X2,high) ),
file('theBenchmark.p',mp_not_high_and_low) ).
% FOF SIMPLE INFERENCE
fof(mp_not_high_and_low_elimTB,axiom,
! [X1,X2] :
~ ( number_of_routines(X1,X2,low)
& number_of_routines(X1,X2,high) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[mp_not_high_and_low])]) ).
% FOF SIMPLE INFERENCE
fof(mp_not_high_and_low_elimImpEquivPushNegMiniScope,axiom,
! [X1,X2] :
( ~ number_of_routines(X1,X2,low)
| ~ number_of_routines(X1,X2,high) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[mp_not_high_and_low_elimTB]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_1,plain,
( ~ number_of_routines(X0,X1,low)
| ~ number_of_routines(X0,X1,high) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[mp_not_high_and_low_elimImpEquivPushNegMiniScope])]) ).
% FILE RECORD
fof(prove_t10,conjecture,
? [X1,X2] :
( organisation_at_time(X1,X2)
& ~ first_mover(X1)
& ~ efficient_producer(X1) ),
file('theBenchmark.p',prove_t10) ).
% NEGATING CONJECTURE
fof(prove_t10_nc,negated_conjecture,
~ ? [X1,X2] :
( organisation_at_time(X1,X2)
& ~ first_mover(X1)
& ~ efficient_producer(X1) ),
inference(negating_conjecture,[status(cth)],[prove_t10]) ).
% FOF SIMPLE INFERENCE
fof(prove_t10_nc_elimTB,negated_conjecture,
~ ? [X1,X2] :
( organisation_at_time(X1,X2)
& ~ first_mover(X1)
& ~ efficient_producer(X1) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[prove_t10_nc])]) ).
% FOF SIMPLE INFERENCE
fof(prove_t10_nc_elimImpEquivPushNegMiniScope,negated_conjecture,
! [X1] :
( ! [X2] : ~ organisation_at_time(X1,X2)
| first_mover(X1)
| efficient_producer(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[prove_t10_nc_elimTB]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_8,plain,
( ~ organisation_at_time(X0,X1)
| first_mover(X0)
| efficient_producer(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[prove_t10_nc_elimImpEquivPushNegMiniScope])]) ).
% FILE RECORD
fof(a14,hypothesis,
! [X1,X2] :
( ( organisation_at_time(X1,X2)
& efficient_producer(X1)
& founding_time(X1,X2) )
=> has_elaborated_routines(X1,X2) ),
file('theBenchmark.p',a14) ).
% FOF SIMPLE INFERENCE
fof(a14_elimTB,hypothesis,
! [X1,X2] :
( ( organisation_at_time(X1,X2)
& efficient_producer(X1)
& founding_time(X1,X2) )
=> has_elaborated_routines(X1,X2) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[a14])]) ).
% FOF SIMPLE INFERENCE
fof(a14_elimImpEquivPushNegMiniScope,hypothesis,
! [X1,X2] :
( ~ organisation_at_time(X1,X2)
| ~ efficient_producer(X1)
| ~ founding_time(X1,X2)
| has_elaborated_routines(X1,X2) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[a14_elimTB]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_2,plain,
( ~ organisation_at_time(X0,X1)
| ~ efficient_producer(X0)
| ~ founding_time(X0,X1)
| has_elaborated_routines(X0,X1) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[a14_elimImpEquivPushNegMiniScope])]) ).
% FILE RECORD
fof(a16,hypothesis,
? [X1,X2] :
( organisation_at_time(X1,X2)
& founding_time(X1,X2)
& number_of_routines(X1,X2,high)
& ~ has_elaborated_routines(X1,X2) ),
file('theBenchmark.p',a16) ).
% FOF SIMPLE INFERENCE
fof(a16_elimTB,hypothesis,
? [X1,X2] :
( organisation_at_time(X1,X2)
& founding_time(X1,X2)
& number_of_routines(X1,X2,high)
& ~ has_elaborated_routines(X1,X2) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[a16])]) ).
% FOF SIMPLE INFERENCE
fof(a16_elimImpEquivPushNegMiniScope,hypothesis,
? [X1,X2] :
( organisation_at_time(X1,X2)
& founding_time(X1,X2)
& number_of_routines(X1,X2,high)
& ~ has_elaborated_routines(X1,X2) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[a16_elimTB]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(a16_skol,hypothesis,
( organisation_at_time(skc1,skc2)
& founding_time(skc1,skc2)
& number_of_routines(skc1,skc2,high)
& ~ has_elaborated_routines(skc1,skc2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skc1,skc2]),skolemize(X1,skc1),skolemize(X2,skc2)],[a16_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_6,plain,
number_of_routines(skc1,skc2,high),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[a16_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_7,plain,
~ has_elaborated_routines(skc1,skc2),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[a16_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_4,plain,
organisation_at_time(skc1,skc2),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[a16_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_5,plain,
founding_time(skc1,skc2),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[a16_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_9,plain,
$false,
inference(resolution,[status(thm)],[c_3,c_1,c_8,c_2,c_6,c_7,c_4,c_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT041+2 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.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 : Mon Sep 7 13:05:30 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37
% 0.09/0.37 % Input Clauses:
% 0.09/0.37 % 1:2:2:INP:TopTop: number_of_routines(x0,x1,low),number_of_routines(x0,x1,high) ->
% 0.09/0.37 % 2:4:2:INP:TopTop: organisation_at_time(x0,x1),efficient_producer(x0),founding_time(x0,x1) -> has_elaborated_routines(x0,x1)
% 0.09/0.37 % 3:4:2:INP:TopTop: organisation_at_time(x0,x1),first_mover(x0),founding_time(x0,x1) -> number_of_routines(x0,x1,low)
% 0.09/0.37 % 4:1:0:INP:: -> organisation_at_time(skc1,skc2)
% 0.09/0.37 % 5:1:0:INP:: -> founding_time(skc1,skc2)
% 0.09/0.37 % 6:1:0:INP:: -> number_of_routines(skc1,skc2,high)
% 0.09/0.37 % 7:1:0:INP:: has_elaborated_routines(skc1,skc2) ->
% 0.09/0.37 % 8:3:2:INP:TopTop: organisation_at_time(x0,x1) -> first_mover(x0),efficient_producer(x0)
% 0.09/0.37
% 0.09/0.37 % Predicates: number_of_routines organisation_at_time efficient_producer founding_time has_elaborated_routines first_mover
% 0.09/0.37 % Fol Constants: low high skc1 skc2
% 0.09/0.37 % Fol Functions:
% 0.09/0.37 % Problem Properties:
% 0.09/0.37 % This is a Bernays Schoenfinkel problem. The Problem is linear.
% 0.09/0.37
% 0.09/0.37
% 0.09/0.37 % Reduced Input Axiom Clauses:
% 0.09/0.37 % 1:2:2:INP:TopTop: number_of_routines(x0,x1,low),number_of_routines(x0,x1,high) ->
% 0.09/0.37
% 0.09/0.37 % Reduced Input Conjecture Clauses:
% 0.09/0.37 % 2:4:2:INP:TopTop: organisation_at_time(x0,x1),efficient_producer(x0),founding_time(x0,x1) -> has_elaborated_routines(x0,x1)
% 0.09/0.37 % 3:4:2:INP:TopTop: organisation_at_time(x0,x1),first_mover(x0),founding_time(x0,x1) -> number_of_routines(x0,x1,low)
% 0.09/0.37 % 4:1:0:INP:: -> organisation_at_time(skc1,skc2)
% 0.09/0.37 % 5:1:0:INP:: -> founding_time(skc1,skc2)
% 0.09/0.37 % 6:1:0:INP:: -> number_of_routines(skc1,skc2,high)
% 0.09/0.37 % 7:1:0:INP:: has_elaborated_routines(skc1,skc2) ->
% 0.09/0.37 % 8:3:2:INP:TopTop: organisation_at_time(x0,x1) -> first_mover(x0),efficient_producer(x0)
% 0.09/0.37
% 0.09/0.37
% 0.09/0.37 % === Starting SPASS-SCL-FOL A Little Less Naive, considering 14 atoms initially. Used heuristic: lmodel_grow ===
% 0.09/0.37
% 0.09/0.37
% 0.09/0.37
% 0.09/0.37 % SZS status Theorem
% 0.09/0.37 % Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37
% 0.09/0.37 % SPASS-SCL-FOL Statistics:
% 0.09/0.37 % Number of learned clauses: 0
% 0.09/0.37 % Number of propagations: 7
% 0.09/0.37 % Number of decisions: 2
% 0.09/0.37 % Number of resolutions: 7
% 0.09/0.37 % Number of condensations: 0
% 0.09/0.37 % Number of sub resolutions: 0
% 0.09/0.37
% 0.09/0.37 % Solver is done. Empty clause found
% 0.09/0.37
% 0.09/0.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.09/0.37 % SZS output start Proof for theBenchmark
% See solution above
% 0.09/0.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.09/0.37
% 0.09/0.37
% 0.09/0.37 % Needed: 0:00:00.00
% 0.09/0.37
% 0.09/0.37 % ###
% 0.09/0.37 % ### Pagesize: 8192
% 0.09/0.37 % ### Marksize: 0
% 0.09/0.37 % ### Memory demanded: 282 KBytes
% 0.09/0.37 % ### Memory freed: 282 KBytes
% 0.09/0.37 % ### Memory remaining: 0 Bytes
% 0.09/0.37 % ### Pages allocated: 118 Pages
% 0.09/0.37 % ###
%------------------------------------------------------------------------------