%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : LCL027-1 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:27:17 PM UTC 2026
% Result : Unsatisfiable 42.18s 8.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL027-1 : TPTP v9.2.1. Released v1.0.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n008.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 12:25:44 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.22/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 42.18/8.94 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.18/8.94 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.18/8.94 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.18/8.94 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.18/8.94 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.18/8.94 Execution resolution_2 ended with status: unsatisfiable
% 42.18/8.94 Used heuristic: resolution_2
% 42.18/8.94
% 42.18/8.94 Input Clauses:
% 42.18/8.94
% 42.18/8.94 Predicates: is_a_theorem
% 42.18/8.94 Fol Constants: falsehood a
% 42.18/8.94 Fol Functions: implies
% 42.18/8.94 Problem Properties:
% 42.18/8.94 This is a full first-order problem without equality.
% 42.18/8.94
% 42.18/8.94 After reduction: Problem Properties:
% 42.18/8.94 This is a full first-order problem without equality.
% 42.18/8.94
% 42.18/8.94
% 42.18/8.94 Reduced Input Clauses:
% 42.18/8.94
% 42.18/8.94 Most General Atoms: is_a_theorem(x1)
% 42.18/8.94
% 42.18/8.94 === Starting SPASS-SCL-FOL A Little Less Naive, considering 46 atoms initially, heuristics mode: resolution_2 ===
% 42.18/8.94
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 46
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Backtracking. Learning clause 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0))
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> a, x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 7:1:0:[6.2,5.1,1.3,6.2,3.1]:: is_a_theorem(falsehood) ->
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 48
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 8:1:4:[6.1,4.1]:TopTopTopTop: -> is_a_theorem(implies(x0,implies(implies(x1,implies(x2,x3)),implies(implies(x1,x2),implies(x1,x3)))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 48
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 50
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood)))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 9:1:5:[6.1,8.1]:TopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(implies(x2,implies(x3,x4)),implies(implies(x2,x3),implies(x2,x4))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 114
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 115
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 10:1:6:[6.1,9.1]:TopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(implies(x3,implies(x4,x5)),implies(implies(x3,x4),implies(x3,x5)))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 117
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood)))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 11:1:7:[6.1,10.1]:TopTopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(x3,implies(implies(x4,implies(x5,x6)),implies(implies(x4,x5),implies(x4,x6))))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 119
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood))))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 12:1:8:[6.1,11.1]:TopTopTopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(x3,implies(x4,implies(implies(x5,implies(x6,x7)),implies(implies(x5,x6),implies(x5,x7)))))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 121
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood)))))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 13:1:9:[6.1,12.1]:TopTopTopTopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(x3,implies(x4,implies(x5,implies(implies(x6,implies(x7,x8)),implies(implies(x6,x7),implies(x6,x8))))))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 185
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 186
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood))))))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 14:1:10:[6.1,13.1]:TopTopTopTopTopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(x3,implies(x4,implies(x5,implies(x6,implies(implies(x7,implies(x8,x9)),implies(implies(x7,x8),implies(x7,x9)))))))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 188
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood)))))))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 15:1:11:[6.1,14.1]:TopTopTopTopTopTopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(x3,implies(x4,implies(x5,implies(x6,implies(x7,implies(implies(x8,implies(x9,x10)),implies(implies(x8,x9),implies(x8,x10))))))))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 190
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood))))))))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 16:1:12:[6.1,15.1]:TopTopTopTopTopTopTopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(x3,implies(x4,implies(x5,implies(x6,implies(x7,implies(x8,implies(implies(x9,implies(x10,x11)),implies(implies(x9,x10),implies(x9,x11)))))))))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 192
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood)))))))))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 17:1:13:[6.1,16.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(x3,implies(x4,implies(x5,implies(x6,implies(x7,implies(x8,implies(x9,implies(implies(x10,implies(x11,x12)),implies(implies(x10,x11),implies(x10,x12))))))))))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 256
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 257
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood))))))))))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 18:1:14:[6.1,17.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(x3,implies(x4,implies(x5,implies(x6,implies(x7,implies(x8,implies(x9,implies(x10,implies(implies(x11,implies(x12,x13)),implies(implies(x11,x12),implies(x11,x13)))))))))))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 259
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood)))))))))))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 19:1:15:[6.1,18.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(x3,implies(x4,implies(x5,implies(x6,implies(x7,implies(x8,implies(x9,implies(x10,implies(x11,implies(implies(x12,implies(x13,x14)),implies(implies(x12,x13),implies(x12,x14))))))))))))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 261
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood))))))))))))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 20:1:16:[6.1,19.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(x3,implies(x4,implies(x5,implies(x6,implies(x7,implies(x8,implies(x9,implies(x10,implies(x11,implies(x12,implies(implies(x13,implies(x14,x15)),implies(implies(x13,x14),implies(x13,x15)))))))))))))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 263
% 42.18/8.94 === Restarting.
% 42.18/8.94 === Conflict found: 6:2:2:[1.1,2.1]:TopTop: is_a_theorem(x0) -> is_a_theorem(implies(x1,x0)) {x0 -> implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(falsehood,implies(implies(falsehood,implies(falsehood,falsehood)),implies(implies(falsehood,falsehood),implies(falsehood,falsehood)))))))))))))))), x1 -> falsehood}
% 42.18/8.94 === Backtracking. Learning clause 21:1:17:[6.1,20.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> is_a_theorem(implies(x0,implies(x1,implies(x2,implies(x3,implies(x4,implies(x5,implies(x6,implies(x7,implies(x8,implies(x9,implies(x10,implies(x11,implies(x12,implies(x13,implies(implies(x14,implies(x15,x16)),implies(implies(x14,x15),implies(x14,x16))))))))))))))))))
% 42.18/8.94 === Clause set with instances from active satisfied. Growing active. New size: 327
% 42.18/8.94 === Backtracking. Learning clause 22:2:3:[1.1,4.1,6.2]:TopTopTop: is_a_theorem(implies(x0,x1)) -> is_a_theorem(implies(implies(x2,x0),implies(x2,x1)))
% 42.18/8.94
% 42.18/8.94 SZS status Unsatisfiable
% 42.18/8.94
% 42.18/8.94 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.18/8.94
% 42.18/8.94 SPASS-SCL-FOL Statistics:
% 42.18/8.94 Number of learned clauses: 17
% 42.18/8.94 Number of propagations: 2596
% 42.18/8.94 Number of decisions: 317
% 42.18/8.94 Number of resolutions: 25
% 42.18/8.94 Number of condensations: 0
% 42.18/8.94 Number of sub resolutions: 0
% 42.18/8.94 Number of input literals (deduplicated): 6
% 42.18/8.94 Number of grows: 20
% 42.18/8.94 Number of considered ground atoms: 327
% 42.18/8.94
% 42.18/8.94 Needed: 0:00:08.39
% 42.18/8.94
%------------------------------------------------------------------------------