%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 7 07:28:54 PM UTC 2026
% Result : Theorem 0.39s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.33 % Computer : n003.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 12:42:27 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.23/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.39/0.59 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.59 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.59 Execution normal ended with status: unsatisfiable
% 0.39/0.59 Used heuristic: normal
% 0.39/0.59
% 0.39/0.59 Input Clauses:
% 0.39/0.59
% 0.39/0.59 Predicates: proh aee aer act tgt activates founds duty bearer cnt part_of right has_rem founds_rem power subjection norm_state_change inst_event triggers competent_for about_event does rem_act agent action target rule event ren1 ren2 ren3 ren4 ren5
% 0.39/0.59 Fol Constants: duty_rem marketplace philharmonie distrib concert_ds f1 e1
% 0.39/0.59 Fol Functions: rfr decl skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12
% 0.39/0.59 Problem Properties:
% 0.39/0.59 This is a full first-order problem without equality.
% 0.39/0.59
% 0.39/0.59 After reduction: Problem Properties:
% 0.39/0.59 This is a full first-order problem without equality.
% 0.39/0.59
% 0.39/0.59
% 0.39/0.59 Reduced Input Clauses:
% 0.39/0.59 53:9:3:[35.4,51.5,36.4,52.10]:TopTopTop: founds_rem(e1,x0,f1),power(x1),bearer(x1,philharmonie),cnt(x1,decl(distrib),concert_ds),part_of(x1,x0),subjection(x2),bearer(x2,marketplace),cnt(x2,decl(distrib),concert_ds),part_of(x2,x0) ->
% 0.39/0.59
% 0.39/0.59 Most General Atoms: ren1(x0,x1,x2,x3,x4,x5,x6,x7,x8) founds(x0,x1,x2) duty(x3) right(x7) cnt(x7,rfr(x5),x6) proh(x0) aer(x0,x2) activates(x5,x0) ren2(x0,x1,x2,x3,x4,x5,x6,x7,x8) has_rem(x0) ren3(x0,x1,x2,x3,x4) inst_event(x0) triggers(x0,x1,x2,x3,x4) norm_state_change(x0,x1,x2,x3) ren4(x0,x1,x2,x3,x4) bearer(x0,x1) competent_for(x0,x1) ren5(x0,x1,x2,x3) rem_act(x0,x1) act(x0,x1) tgt(x0,x2) aee(x0,x3) does(x3,x1,x2) cnt(x0,decl(x1),x2) founds_rem(x4,x3,x5) about_event(x0,x4) agent(marketplace) agent(philharmonie) action(distrib) target(concert_ds) rule(f1) event(e1) power(x1) subjection(x2) part_of(x2,x0)
% 0.39/0.59
% 0.39/0.59 === Starting SPASS-SCL-FOL A Little Less Naive, considering 54 atoms initially, heuristics mode: normal ===
% 0.39/0.59
% 0.39/0.59 === Clause set with instances from active satisfied. Growing active. New size: 118
% 0.39/0.59 === Clause set with instances from active satisfied. Growing active. New size: 182
% 0.39/0.59 === Conflict found: 53:9:3:[35.4,51.5,36.4,52.10]:TopTopTop: founds_rem(e1,x0,f1),power(x1),bearer(x1,philharmonie),cnt(x1,decl(distrib),concert_ds),part_of(x1,x0),subjection(x2),bearer(x2,marketplace),cnt(x2,decl(distrib),concert_ds),part_of(x2,x0) -> {x0 -> skf4(f1,marketplace,philharmonie,distrib,concert_ds,e1), x1 -> skf5(f1,marketplace,philharmonie,distrib,concert_ds,e1), x2 -> skf6(f1,marketplace,philharmonie,distrib,concert_ds,e1)}
% 0.39/0.59
% 0.39/0.59 SZS status Unsatisfiable
% 0.39/0.59
% 0.39/0.59 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.59
% 0.39/0.59 SPASS-SCL-FOL Statistics:
% 0.39/0.59 Number of learned clauses: 0
% 0.39/0.59 Number of propagations: 91
% 0.39/0.59 Number of decisions: 60
% 0.39/0.59 Number of resolutions: 17
% 0.39/0.59 Number of condensations: 0
% 0.39/0.59 Number of sub resolutions: 2
% 0.39/0.59 Number of input literals (deduplicated): 54
% 0.39/0.59 Number of grows: 2
% 0.39/0.59 Number of considered ground atoms: 182
% 0.39/0.59
% 0.39/0.59 Needed: 0:00:00.01
% 0.39/0.59
%------------------------------------------------------------------------------