%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : CSR062+1 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:20:01 PM UTC 2026
% Result : Theorem 0.31s 0.98s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.53 % Problem : CSR062+1 : TPTP v9.2.1. Released v3.4.0.
% 0.01/0.54 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.75 % Computer : n001.cluster.edu
% 0.14/0.75 % Model : x86_64 x86_64
% 0.14/0.75 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.75 % Memory : 8042.1875MB
% 0.14/0.75 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.75 % CPULimit : 300
% 0.14/0.75 % WCLimit : 300
% 0.14/0.75 % DateTime : Thu May 7 11:42:16 EDT 2026
% 0.14/0.76 % CPUTime :
% 0.14/0.76 SPASS-SCL-FOL version:
% 0.20/0.85 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.31/0.98 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.98 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.98 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.98 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.98 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.98 Execution resolution_1 ended with status: unsatisfiable
% 0.31/0.98 Used heuristic: resolution_1
% 0.31/0.98
% 0.31/0.98 Input Clauses:
% 0.31/0.98
% 0.31/0.98 Predicates: genlmt transitivebinarypredicate genlpreds tptptypes_6_388 tptptypes_5_387 genlinverse tptptypes_7_389 tptptypes_8_390 mtvisible isa disjointwith collection genls tptpcol_15_4027 pushingwithfingers firstordercollection binarypredicate predicate thing microtheory
% 0.31/0.98 Fol Constants: c_calendarsmt c_calendarsvocabularymt c_genlmt c_basekb c_universalvocabularymt c_cyclistsmt c_tptptypes_6_388 c_tptptypes_5_387 c_tptptypes_7_389 c_tptptypes_8_390 c_tptp_spindleheadmt c_tptp_member3205_mt c_pushingwithfingers c_tptpcol_15_4027 c_transitivebinarypredicate
% 0.31/0.98 Fol Functions:
% 0.31/0.98 Problem Properties:
% 0.31/0.98 This is a Bernays Schoenfinkel problem.
% 0.31/0.98
% 0.31/0.98 After reduction: Problem Properties:
% 0.31/0.98 This is a Bernays Schoenfinkel problem.
% 0.31/0.98
% 0.31/0.98
% 0.31/0.98 Reduced Input Clauses:
% 0.31/0.98
% 0.31/0.98 Most General Atoms: tptptypes_5_387(x0,x1) tptptypes_7_389(x0,x1) tptptypes_6_388(x1,x0) tptptypes_8_390(x0,x1) isa(x0,x2) collection(x0) disjointwith(x2,x1) tptpcol_15_4027(x0) pushingwithfingers(x0) firstordercollection(x0) binarypredicate(x0) genlinverse(x0,x2) genlpreds(x0,x1) predicate(x0) transitivebinarypredicate(x0) genlmt(x0,x2) thing(x0) genls(x1,x2) mtvisible(x1) microtheory(x1)
% 0.31/0.98
% 0.31/0.98 === Starting SPASS-SCL-FOL A Little Less Naive, considering 61 atoms initially, heuristics mode: resolution_1 ===
% 0.31/0.98
% 0.31/0.98 === Backtracking. Learning clause 64:2:1:[58.2,3.1]:Top: genlmt(x0,c_basekb) -> genlmt(x0,c_universalvocabularymt)
% 0.31/0.98 === Backtracking. Learning clause 65:2:1:[58.1,12.1]:Top: genlmt(c_cyclistsmt,x0) -> genlmt(c_tptp_spindleheadmt,x0)
% 0.31/0.98 === Backtracking. Learning clause 66:2:1:[58.1,13.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3205_mt,x0)
% 0.31/0.98 === Backtracking. Learning clause 67:1:0:[39.1,6.1]:: -> predicate(c_tptptypes_5_387)
% 0.31/0.98 === Backtracking. Learning clause 68:1:0:[41.1,6.1]:: -> predicate(c_tptptypes_6_388)
% 0.31/0.98 === Backtracking. Learning clause 69:1:0:[39.1,10.1]:: -> predicate(c_tptptypes_7_389)
% 0.31/0.98 === Backtracking. Learning clause 70:1:0:[41.1,10.1]:: -> predicate(c_tptptypes_8_390)
% 0.31/0.98 === Backtracking. Learning clause 71:1:0:[30.1,8.1]:: -> binarypredicate(c_tptptypes_6_388)
% 0.31/0.98 === Backtracking. Learning clause 72:1:0:[31.1,8.1]:: -> binarypredicate(c_tptptypes_7_389)
% 0.31/0.98 === Backtracking. Learning clause 73:2:0:[26.1,14.2]:: mtvisible(c_cyclistsmt) -> firstordercollection(c_tptpcol_15_4027)
% 0.31/0.98 === Backtracking. Learning clause 74:2:0:[27.1,14.2]:: mtvisible(c_cyclistsmt) -> firstordercollection(c_pushingwithfingers)
% 0.31/0.98 === Backtracking. Learning clause 75:2:0:[11.1,14.2]:: mtvisible(c_cyclistsmt) -> tptptypes_7_389(c_pushingwithfingers,c_tptpcol_15_4027)
% 0.31/0.98 === Clause set with instances from active satisfied. Growing active. New size: 75
% 0.31/0.98 === Restarting.
% 0.31/0.98 === Backtracking. Learning clause 76:1:0:[57.1,4.1]:: -> microtheory(c_cyclistsmt)
% 0.31/0.98 === Conflict found: 65:2:1:[58.1,12.1]:Top: genlmt(c_cyclistsmt,x0) -> genlmt(c_tptp_spindleheadmt,x0) {x0 -> c_calendarsmt}
% 0.31/0.98 === Backtracking. Learning clause 77:1:0:[65.2,57.1,4.1]:: -> microtheory(c_tptp_spindleheadmt)
% 0.31/0.98 === Conflict found: 66:2:1:[58.1,13.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3205_mt,x0) {x0 -> c_calendarsmt}
% 0.31/0.98 === Backtracking. Learning clause 78:1:0:[66.2,53.2,65.2,4.1,62.1]:: -> mtvisible(c_calendarsmt)
% 0.31/0.98 === Backtracking. Learning clause 79:1:0:[53.2,13.1,62.1]:: -> mtvisible(c_tptp_spindleheadmt)
% 0.31/0.98 === Backtracking. Learning clause 80:1:0:[53.2,12.1,79.1]:: -> mtvisible(c_cyclistsmt)
% 0.31/0.98 === Backtracking. Learning clause 81:2:1:[42.1,10.1]:Top: genlpreds(c_tptptypes_7_389,x0) -> genlpreds(c_tptptypes_8_390,x0)
% 0.31/0.98 === Backtracking. Learning clause 82:2:1:[42.2,10.1]:Top: genlpreds(x0,c_tptptypes_8_390) -> genlpreds(x0,c_tptptypes_7_389)
% 0.31/0.98 === Backtracking. Learning clause 83:2:1:[33.1,8.1,30.1]:Top: genlpreds(c_tptptypes_6_388,x0) -> binarypredicate(x0)
% 0.31/0.98 === Clause set with instances from active satisfied. Growing active. New size: 79
% 0.31/0.98 === Restarting.
% 0.31/0.98 === Backtracking. Learning clause 84:1:0:[58.2,5.1,55.1,1.1]:: -> microtheory(c_basekb)
% 0.31/0.98 === Backtracking. Learning clause 85:2:1:[58.2,5.1]:Top: genlmt(x0,c_calendarsvocabularymt) -> genlmt(x0,c_basekb)
% 0.31/0.98 === Conflict found: 64:2:1:[58.2,3.1]:Top: genlmt(x0,c_basekb) -> genlmt(x0,c_universalvocabularymt) {x0 -> c_calendarsmt}
% 0.31/0.98 === Backtracking. Learning clause 86:1:0:[64.2,55.1,85.2,1.1]:: -> microtheory(c_universalvocabularymt)
% 0.31/0.98 === Backtracking. Learning clause 87:2:1:[58.2,12.1]:Top: genlmt(x0,c_tptp_spindleheadmt) -> genlmt(x0,c_cyclistsmt)
% 0.31/0.98 === Conflict found: 66:2:1:[58.1,13.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3205_mt,x0) {x0 -> c_calendarsmt}
% 0.31/0.98 === Backtracking. Learning clause 88:1:0:[66.2,57.1,65.2,4.1]:: -> microtheory(c_tptp_member3205_mt)
% 0.31/0.98 === Backtracking. Learning clause 89:2:1:[58.2,13.1]:Top: genlmt(x0,c_tptp_member3205_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 0.31/0.98 === Backtracking. Learning clause 90:1:1:[7.2,63.1]:Top: tptptypes_6_388(x0,c_pushingwithfingers) ->
% 0.31/0.98 === Backtracking. Learning clause 91:2:1:[16.2,8.1]:Top: genlinverse(x0,c_tptptypes_7_389) -> genlpreds(x0,c_tptptypes_6_388)
% 0.31/0.98
% 0.31/0.98 SZS status Unsatisfiable
% 0.31/0.98
% 0.31/0.98 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.98
% 0.31/0.98 SPASS-SCL-FOL Statistics:
% 0.31/0.98 Number of learned clauses: 28
% 0.31/0.98 Number of propagations: 700
% 0.31/0.98 Number of decisions: 479
% 0.31/0.98 Number of resolutions: 44
% 0.31/0.98 Number of condensations: 0
% 0.31/0.98 Number of sub resolutions: 0
% 0.31/0.98 Number of input literals (deduplicated): 41
% 0.31/0.98 Number of grows: 2
% 0.31/0.98 Number of considered ground atoms: 79
% 0.31/0.98
% 0.31/0.98 Needed: 0:00:00.02
% 0.31/0.98
%------------------------------------------------------------------------------