%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : LCL098-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 : n022.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:22 PM UTC 2026
% Result : Unsatisfiable 5.31s 1.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL098-1 : TPTP v9.2.1. Released v1.0.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n022.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % 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:26:51 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 5.31/1.56 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.31/1.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.31/1.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.31/1.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.31/1.56 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.31/1.56 Execution resolution_2 ended with status: unsatisfiable
% 5.31/1.56 Used heuristic: resolution_2
% 5.31/1.56
% 5.31/1.56 Input Clauses:
% 5.31/1.56
% 5.31/1.56 Predicates: is_a_theorem
% 5.31/1.56 Fol Constants: a b c e falsehood
% 5.31/1.56 Fol Functions: equivalent
% 5.31/1.56 Problem Properties:
% 5.31/1.56 This is a full first-order problem without equality.
% 5.31/1.56
% 5.31/1.56 After reduction: Problem Properties:
% 5.31/1.56 This is a full first-order problem without equality.
% 5.31/1.56
% 5.31/1.56
% 5.31/1.56 Reduced Input Clauses:
% 5.31/1.56
% 5.31/1.56 Most General Atoms: is_a_theorem(x1)
% 5.31/1.56
% 5.31/1.56 === Starting SPASS-SCL-FOL A Little Less Naive, considering 40 atoms initially, heuristics mode: resolution_2 ===
% 5.31/1.56
% 5.31/1.56 === Clause set with instances from active satisfied. Growing active. New size: 41
% 5.31/1.56 === Restarting.
% 5.31/1.56 === Backtracking. Learning clause 4:2:5:[1.1,2.1]:TopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),x4)) -> is_a_theorem(x4)
% 5.31/1.56 === Clause set with instances from active satisfied. Growing active. New size: 43
% 5.31/1.56 === Restarting.
% 5.31/1.56 === Conflict found: 4:2:5:[1.1,2.1]:TopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),x4)) -> is_a_theorem(x4) {x0 -> a, x1 -> a, x2 -> a, x3 -> a, x4 -> equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))}
% 5.31/1.56 === Backtracking. Learning clause 5:1:4:[4.2,3.1]:TopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))) ->
% 5.31/1.56 === Clause set with instances from active satisfied. Growing active. New size: 45
% 5.31/1.56 === Restarting.
% 5.31/1.56 === Conflict found: 4:2:5:[1.1,2.1]:TopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),x4)) -> is_a_theorem(x4) {x0 -> a, x1 -> a, x2 -> a, x3 -> a, x4 -> equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))}
% 5.31/1.56 === Backtracking. Learning clause 6:1:8:[4.2,5.1]:TopTopTopTopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),equivalent(equivalent(equivalent(equivalent(equivalent(x4,x5),equivalent(x4,x6)),x7),equivalent(equivalent(x5,x6),x7)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))) ->
% 5.31/1.56 === Clause set with instances from active satisfied. Growing active. New size: 47
% 5.31/1.56 === Restarting.
% 5.31/1.56 === Conflict found: 4:2:5:[1.1,2.1]:TopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),x4)) -> is_a_theorem(x4) {x0 -> a, x1 -> a, x2 -> a, x3 -> a, x4 -> equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))}
% 5.31/1.56 === Backtracking. Learning clause 7:1:12:[4.2,6.1]:TopTopTopTopTopTopTopTopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),equivalent(equivalent(equivalent(equivalent(equivalent(x4,x5),equivalent(x4,x6)),x7),equivalent(equivalent(x5,x6),x7)),equivalent(equivalent(equivalent(equivalent(equivalent(x8,x9),equivalent(x8,x10)),x11),equivalent(equivalent(x9,x10),x11)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))))) ->
% 5.31/1.56 === Clause set with instances from active satisfied. Growing active. New size: 111
% 5.31/1.56 === Clause set with instances from active satisfied. Growing active. New size: 113
% 5.31/1.56 === Restarting.
% 5.31/1.56 === Conflict found: 4:2:5:[1.1,2.1]:TopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),x4)) -> is_a_theorem(x4) {x0 -> a, x1 -> a, x2 -> a, x3 -> a, x4 -> equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))))}
% 5.31/1.56 === Backtracking. Learning clause 8:1:16:[4.2,7.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),equivalent(equivalent(equivalent(equivalent(equivalent(x4,x5),equivalent(x4,x6)),x7),equivalent(equivalent(x5,x6),x7)),equivalent(equivalent(equivalent(equivalent(equivalent(x8,x9),equivalent(x8,x10)),x11),equivalent(equivalent(x9,x10),x11)),equivalent(equivalent(equivalent(equivalent(equivalent(x12,x13),equivalent(x12,x14)),x15),equivalent(equivalent(x13,x14),x15)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))))) ->
% 5.31/1.56 === Clause set with instances from active satisfied. Growing active. New size: 115
% 5.31/1.56 === Restarting.
% 5.31/1.56 === Conflict found: 4:2:5:[1.1,2.1]:TopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),x4)) -> is_a_theorem(x4) {x0 -> a, x1 -> a, x2 -> a, x3 -> a, x4 -> equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))))}
% 5.31/1.56 === Backtracking. Learning clause 9:1:20:[4.2,8.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),equivalent(equivalent(equivalent(equivalent(equivalent(x4,x5),equivalent(x4,x6)),x7),equivalent(equivalent(x5,x6),x7)),equivalent(equivalent(equivalent(equivalent(equivalent(x8,x9),equivalent(x8,x10)),x11),equivalent(equivalent(x9,x10),x11)),equivalent(equivalent(equivalent(equivalent(equivalent(x12,x13),equivalent(x12,x14)),x15),equivalent(equivalent(x13,x14),x15)),equivalent(equivalent(equivalent(equivalent(equivalent(x16,x17),equivalent(x16,x18)),x19),equivalent(equivalent(x17,x18),x19)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))))))) ->
% 5.31/1.56 === Clause set with instances from active satisfied. Growing active. New size: 117
% 5.31/1.56 === Restarting.
% 5.31/1.56 === Conflict found: 4:2:5:[1.1,2.1]:TopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),x4)) -> is_a_theorem(x4) {x0 -> a, x1 -> a, x2 -> a, x3 -> a, x4 -> equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))))))}
% 5.31/1.56 === Backtracking. Learning clause 10:1:24:[4.2,9.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),equivalent(equivalent(equivalent(equivalent(equivalent(x4,x5),equivalent(x4,x6)),x7),equivalent(equivalent(x5,x6),x7)),equivalent(equivalent(equivalent(equivalent(equivalent(x8,x9),equivalent(x8,x10)),x11),equivalent(equivalent(x9,x10),x11)),equivalent(equivalent(equivalent(equivalent(equivalent(x12,x13),equivalent(x12,x14)),x15),equivalent(equivalent(x13,x14),x15)),equivalent(equivalent(equivalent(equivalent(equivalent(x16,x17),equivalent(x16,x18)),x19),equivalent(equivalent(x17,x18),x19)),equivalent(equivalent(equivalent(equivalent(equivalent(x20,x21),equivalent(x20,x22)),x23),equivalent(equivalent(x21,x22),x23)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))))))) ->
% 5.31/1.56 === Clause set with instances from active satisfied. Growing active. New size: 119
% 5.31/1.56 === Restarting.
% 5.31/1.56 === Conflict found: 4:2:5:[1.1,2.1]:TopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),x4)) -> is_a_theorem(x4) {x0 -> a, x1 -> a, x2 -> a, x3 -> a, x4 -> equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(equivalent(a,a),equivalent(a,a)),a),equivalent(equivalent(a,a),a)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))))))}
% 5.31/1.56 === Backtracking. Learning clause 11:1:28:[4.2,10.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),equivalent(equivalent(equivalent(equivalent(equivalent(x4,x5),equivalent(x4,x6)),x7),equivalent(equivalent(x5,x6),x7)),equivalent(equivalent(equivalent(equivalent(equivalent(x8,x9),equivalent(x8,x10)),x11),equivalent(equivalent(x9,x10),x11)),equivalent(equivalent(equivalent(equivalent(equivalent(x12,x13),equivalent(x12,x14)),x15),equivalent(equivalent(x13,x14),x15)),equivalent(equivalent(equivalent(equivalent(equivalent(x16,x17),equivalent(x16,x18)),x19),equivalent(equivalent(x17,x18),x19)),equivalent(equivalent(equivalent(equivalent(equivalent(x20,x21),equivalent(x20,x22)),x23),equivalent(equivalent(x21,x22),x23)),equivalent(equivalent(equivalent(equivalent(equivalent(x24,x25),equivalent(x24,x26)),x27),equivalent(equivalent(x25,x26),x27)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))))))))) ->
% 5.31/1.56 === Clause set with instances from active satisfied. Growing active. New size: 183
% 5.31/1.56 === Clause set with instances from active satisfied. Growing active. New size: 186
% 5.31/1.56 === Restarting.
% 5.31/1.56 === Conflict found: 11:1:28:[4.2,10.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(x0,x1),equivalent(x0,x2)),x3),equivalent(equivalent(x1,x2),x3)),equivalent(equivalent(equivalent(equivalent(equivalent(x4,x5),equivalent(x4,x6)),x7),equivalent(equivalent(x5,x6),x7)),equivalent(equivalent(equivalent(equivalent(equivalent(x8,x9),equivalent(x8,x10)),x11),equivalent(equivalent(x9,x10),x11)),equivalent(equivalent(equivalent(equivalent(equivalent(x12,x13),equivalent(x12,x14)),x15),equivalent(equivalent(x13,x14),x15)),equivalent(equivalent(equivalent(equivalent(equivalent(x16,x17),equivalent(x16,x18)),x19),equivalent(equivalent(x17,x18),x19)),equivalent(equivalent(equivalent(equivalent(equivalent(x20,x21),equivalent(x20,x22)),x23),equivalent(equivalent(x21,x22),x23)),equivalent(equivalent(equivalent(equivalent(equivalent(x24,x25),equivalent(x24,x26)),x27),equivalent(equivalent(x25,x26),x27)),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))))))))) -> {x0 -> equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))),equivalent(equivalent(equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))), x1 -> equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))),equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e),equivalent(equivalent(b,falsehood),e)),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))), x2 -> equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))),equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e),equivalent(equivalent(b,falsehood),e)),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))), x3 -> equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))),equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e),equivalent(equivalent(b,falsehood),e)),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))),equivalent(equivalent(equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))),equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e),equivalent(equivalent(b,falsehood),e)),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))))))), x4 -> equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))), x5 -> equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))), x6 -> equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))), x7 -> equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e),equivalent(equivalent(b,falsehood),e)),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e))))), x8 -> equivalent(equivalent(a,falsehood),c), x9 -> equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e), x10 -> equivalent(equivalent(b,falsehood),e), x11 -> equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))), x12 -> equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)), x13 -> equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)), x14 -> equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)), x15 -> equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),equivalent(equivalent(a,b),c)),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e))),equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))), x16 -> equivalent(equivalent(a,b),equivalent(a,falsehood)), x17 -> equivalent(equivalent(a,b),c), x18 -> e, x19 -> equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)), x20 -> a, x21 -> b, x22 -> falsehood, x23 -> e, x24 -> equivalent(a,b), x25 -> equivalent(a,falsehood), x26 -> c, x27 -> equivalent(equivalent(equivalent(a,b),equivalent(a,falsehood)),e)}
% 5.31/1.56
% 5.31/1.56 SZS status Unsatisfiable
% 5.31/1.56
% 5.31/1.56 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.31/1.56
% 5.31/1.56 SPASS-SCL-FOL Statistics:
% 5.31/1.56 Number of learned clauses: 8
% 5.31/1.56 Number of propagations: 511
% 5.31/1.56 Number of decisions: 331
% 5.31/1.56 Number of resolutions: 9
% 5.31/1.56 Number of condensations: 0
% 5.31/1.56 Number of sub resolutions: 0
% 5.31/1.56 Number of input literals (deduplicated): 4
% 5.31/1.56 Number of grows: 11
% 5.31/1.56 Number of considered ground atoms: 186
% 5.31/1.56
% 5.31/1.56 Needed: 0:00:01.04
% 5.31/1.56
%------------------------------------------------------------------------------