%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN311-1 : TPTP v9.2.1. Released v1.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:39:33 PM UTC 2026
% Result : Unsatisfiable 2.21s 0.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN311-1 : TPTP v9.2.1. Released v1.2.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n006.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:40:17 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 2.21/0.97 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.21/0.97 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.21/0.97 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.21/0.97 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.21/0.97 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.21/0.97 Execution resolution_1 ended with status: unsatisfiable
% 2.21/0.97 Used heuristic: resolution_1
% 2.21/0.97
% 2.21/0.97 Input Clauses:
% 2.21/0.97
% 2.21/0.97 Predicates: p
% 2.21/0.97 Fol Constants: a b c d
% 2.21/0.97 Fol Functions: g f
% 2.21/0.97 Problem Properties:
% 2.21/0.97 This is a full first-order problem without equality.
% 2.21/0.97
% 2.21/0.97 After reduction: Problem Properties:
% 2.21/0.97 This is a full first-order problem without equality.
% 2.21/0.97
% 2.21/0.97
% 2.21/0.97 Reduced Input Clauses:
% 2.21/0.97
% 2.21/0.97 Most General Atoms: p(x3,x2,x1,x0)
% 2.21/0.97
% 2.21/0.97 === Starting SPASS-SCL-FOL A Little Less Naive, considering 8 atoms initially, heuristics mode: resolution_1 ===
% 2.21/0.97
% 2.21/0.97 === Backtracking. Learning clause 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2)
% 2.21/0.97 === Backtracking. Learning clause 8:2:4:[2.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,x2,x1,f(x0))
% 2.21/0.97 === Backtracking. Learning clause 9:1:0:[1.2,6.1]:: p(f(g(c)),f(g(b)),f(g(a)),f(g(d))) ->
% 2.21/0.97 === Backtracking. Learning clause 10:1:0:[2.2,6.1,8.2]:: p(g(d),f(g(c)),f(g(b)),f(g(a))) ->
% 2.21/0.97 === Backtracking. Learning clause 11:1:0:[2.2,6.1]:: p(f(g(a)),f(g(b)),f(g(c)),f(g(d))) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 17
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Conflict found: 8:2:4:[2.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,x2,x1,f(x0)) {x0 -> g(a), x1 -> f(g(b)), x2 -> f(g(c)), x3 -> g(d)}
% 2.21/0.97 === Backtracking. Learning clause 12:1:0:[8.2,10.1]:: p(g(a),f(g(b)),f(g(c)),g(d)) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(b), x1 -> f(g(c)), x2 -> f(g(d)), x3 -> f(g(a))}
% 2.21/0.97 === Backtracking. Learning clause 13:1:0:[7.2,11.1]:: p(g(b),f(g(c)),f(g(d)),f(g(a))) ->
% 2.21/0.97 === Backtracking. Learning clause 14:1:0:[4.2,9.1]:: p(g(c),f(g(b)),f(g(a)),f(g(d))) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 23
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Backtracking. Learning clause 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0)
% 2.21/0.97 === Conflict found: 8:2:4:[2.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,x2,x1,f(x0)) {x0 -> g(a), x1 -> f(g(d)), x2 -> f(g(c)), x3 -> g(b)}
% 2.21/0.97 === Backtracking. Learning clause 16:1:0:[8.2,13.1]:: p(g(a),f(g(d)),f(g(c)),g(b)) ->
% 2.21/0.97 === Conflict found: 8:2:4:[2.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,x2,x1,f(x0)) {x0 -> g(d), x1 -> f(g(a)), x2 -> f(g(b)), x3 -> g(c)}
% 2.21/0.97 === Backtracking. Learning clause 17:1:0:[8.2,14.1,2.2]:: p(g(c),f(g(b)),f(g(a)),g(d)) ->
% 2.21/0.97 === Backtracking. Learning clause 18:1:0:[4.2,11.1]:: p(g(a),f(g(b)),f(g(c)),f(g(d))) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(b), x1 -> f(g(a)), x2 -> f(g(d)), x3 -> f(g(c))}
% 2.21/0.97 === Backtracking. Learning clause 19:1:0:[7.2,9.1]:: p(g(b),f(g(a)),f(g(d)),f(g(c))) ->
% 2.21/0.97 === Conflict found: 8:2:4:[2.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,x2,x1,f(x0)) {x0 -> g(d), x1 -> f(g(a)), x2 -> f(g(b)), x3 -> f(g(c))}
% 2.21/0.97 === Backtracking. Learning clause 20:1:0:[8.2,9.1]:: p(g(d),f(g(a)),f(g(b)),f(g(c))) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 30
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(b), x1 -> f(g(c)), x2 -> g(d), x3 -> g(a)}
% 2.21/0.97 === Backtracking. Learning clause 21:1:0:[7.2,12.1]:: p(g(b),f(g(c)),g(d),g(a)) ->
% 2.21/0.97 === Backtracking. Learning clause 22:1:0:[3.2,12.1]:: p(g(a),f(g(b)),f(g(c)),d) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(d), x1 -> f(g(c)), x2 -> g(b), x3 -> g(a)}
% 2.21/0.97 === Backtracking. Learning clause 23:1:0:[7.2,16.1]:: p(g(d),f(g(c)),g(b),g(a)) ->
% 2.21/0.97 === Backtracking. Learning clause 24:1:0:[3.2,16.1]:: p(g(a),f(g(d)),f(g(c)),b) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(b), x1 -> f(g(a)), x2 -> g(d), x3 -> g(c)}
% 2.21/0.97 === Backtracking. Learning clause 25:1:0:[7.2,17.1]:: p(g(b),f(g(a)),g(d),g(c)) ->
% 2.21/0.97 === Backtracking. Learning clause 26:1:0:[3.2,17.1]:: p(g(c),f(g(b)),f(g(a)),d) ->
% 2.21/0.97 === Backtracking. Learning clause 27:1:0:[1.2,9.1,1.2]:: p(f(g(a)),f(g(d)),f(g(c)),f(g(b))) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 48
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Backtracking. Learning clause 28:1:0:[2.2,22.1]:: p(d,f(g(c)),f(g(b)),g(a)) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(d), x1 -> f(g(c)), x2 -> b, x3 -> g(a)}
% 2.21/0.97 === Backtracking. Learning clause 29:1:0:[7.2,24.1]:: p(g(d),f(g(c)),b,g(a)) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(a), x1 -> g(d), x2 -> g(c), x3 -> g(b)}
% 2.21/0.97 === Backtracking. Learning clause 30:1:0:[7.2,25.1]:: p(g(a),g(d),g(c),g(b)) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(c), x1 -> g(d), x2 -> g(a), x3 -> g(b)}
% 2.21/0.97 === Backtracking. Learning clause 31:1:0:[7.2,21.1]:: p(g(c),g(d),g(a),g(b)) ->
% 2.21/0.97 === Backtracking. Learning clause 32:1:0:[2.2,21.1]:: p(g(a),g(d),f(g(c)),g(b)) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> g(a), x1 -> g(b), x2 -> f(g(c)), x3 -> g(d)}
% 2.21/0.97 === Backtracking. Learning clause 33:1:0:[15.2,21.1]:: p(g(a),g(b),f(g(c)),g(d)) ->
% 2.21/0.97 === Backtracking. Learning clause 34:1:0:[3.2,21.1]:: p(g(b),f(g(c)),g(d),a) ->
% 2.21/0.97 === Backtracking. Learning clause 35:1:0:[2.2,26.1]:: p(d,f(g(a)),f(g(b)),g(c)) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(c), x1 -> g(b), x2 -> g(a), x3 -> g(d)}
% 2.21/0.97 === Backtracking. Learning clause 36:1:0:[7.2,23.1]:: p(g(c),g(b),g(a),g(d)) ->
% 2.21/0.97 === Backtracking. Learning clause 37:1:0:[4.2,27.1]:: p(g(a),f(g(d)),f(g(c)),f(g(b))) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 65
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Backtracking. Learning clause 38:1:0:[3.2,30.1]:: p(g(a),g(d),g(c),b) ->
% 2.21/0.97 === Backtracking. Learning clause 39:1:0:[2.2,34.1]:: p(a,g(d),f(g(c)),g(b)) ->
% 2.21/0.97 === Backtracking. Learning clause 40:1:0:[2.2,29.1]:: p(g(a),b,f(g(c)),g(d)) ->
% 2.21/0.97 === Backtracking. Learning clause 41:1:0:[3.2,29.1]:: p(g(d),f(g(c)),b,a) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(a), x1 -> f(g(b)), x2 -> g(c), x3 -> d}
% 2.21/0.97 === Backtracking. Learning clause 42:1:0:[7.2,35.1]:: p(g(a),f(g(b)),g(c),d) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(c), x1 -> f(g(b)), x2 -> g(a), x3 -> d}
% 2.21/0.97 === Backtracking. Learning clause 43:1:0:[7.2,28.1]:: p(g(c),f(g(b)),g(a),d) ->
% 2.21/0.97 === Backtracking. Learning clause 44:1:0:[3.2,28.1]:: p(d,f(g(c)),f(g(b)),a) ->
% 2.21/0.97 === Backtracking. Learning clause 45:1:0:[2.2,24.1]:: p(b,f(g(c)),f(g(d)),g(a)) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> b, x1 -> g(a), x2 -> f(g(d)), x3 -> f(g(c))}
% 2.21/0.97 === Backtracking. Learning clause 46:1:0:[15.2,24.1]:: p(b,g(a),f(g(d)),f(g(c))) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 81
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Backtracking. Learning clause 47:1:0:[2.2,38.1]:: p(b,g(c),g(d),g(a)) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> b, x1 -> g(a), x2 -> g(d), x3 -> g(c)}
% 2.21/0.97 === Backtracking. Learning clause 48:1:0:[15.2,38.1]:: p(b,g(a),g(d),g(c)) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(c), x1 -> b, x2 -> a, x3 -> g(d)}
% 2.21/0.97 === Backtracking. Learning clause 49:1:0:[7.2,41.1]:: p(g(c),b,a,g(d)) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(c), x1 -> f(g(b)), x2 -> a, x3 -> d}
% 2.21/0.97 === Backtracking. Learning clause 50:1:0:[7.2,44.1]:: p(g(c),f(g(b)),a,d) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> a, x1 -> d, x2 -> f(g(c)), x3 -> f(g(b))}
% 2.21/0.97 === Backtracking. Learning clause 51:1:0:[15.2,44.1]:: p(a,d,f(g(c)),f(g(b))) ->
% 2.21/0.97 === Backtracking. Learning clause 52:1:0:[1.2,40.1]:: p(b,f(g(c)),g(d),g(a)) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(b), x1 -> g(c), x2 -> d, x3 -> g(a)}
% 2.21/0.97 === Backtracking. Learning clause 53:1:0:[7.2,42.1]:: p(g(b),g(c),d,g(a)) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> d, x1 -> g(a), x2 -> f(g(b)), x3 -> g(c)}
% 2.21/0.97 === Backtracking. Learning clause 54:1:0:[15.2,42.1]:: p(d,g(a),f(g(b)),g(c)) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> a, x1 -> g(b), x2 -> f(g(c)), x3 -> g(d)}
% 2.21/0.97 === Backtracking. Learning clause 55:1:0:[15.2,34.1]:: p(a,g(b),f(g(c)),g(d)) ->
% 2.21/0.97 === Backtracking. Learning clause 56:1:0:[3.2,45.1]:: p(b,f(g(c)),f(g(d)),a) ->
% 2.21/0.97 === Backtracking. Learning clause 57:1:0:[3.2,35.1]:: p(d,f(g(a)),f(g(b)),c) ->
% 2.21/0.97 === Backtracking. Learning clause 58:1:0:[3.2,33.1]:: p(g(a),g(b),f(g(c)),d) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> d, x1 -> g(a), x2 -> f(g(b)), x3 -> f(g(c))}
% 2.21/0.97 === Backtracking. Learning clause 59:1:0:[15.2,22.1]:: p(d,g(a),f(g(b)),f(g(c))) ->
% 2.21/0.97 === Backtracking. Learning clause 60:1:0:[3.2,25.1]:: p(g(b),f(g(a)),g(d),c) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> d, x1 -> g(c), x2 -> f(g(b)), x3 -> f(g(a))}
% 2.21/0.97 === Backtracking. Learning clause 61:1:0:[15.2,26.1]:: p(d,g(c),f(g(b)),f(g(a))) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 106
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Backtracking. Learning clause 62:1:0:[3.2,49.1]:: p(g(c),b,a,d) ->
% 2.21/0.97 === Backtracking. Learning clause 63:1:0:[3.2,48.1]:: p(b,g(a),g(d),c) ->
% 2.21/0.97 === Backtracking. Learning clause 64:1:0:[2.2,53.1]:: p(g(a),d,g(c),g(b)) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> g(a), x1 -> g(b), x2 -> g(c), x3 -> d}
% 2.21/0.97 === Backtracking. Learning clause 65:1:0:[15.2,53.1]:: p(g(a),g(b),g(c),d) ->
% 2.21/0.97 === Backtracking. Learning clause 66:1:0:[3.2,53.1]:: p(g(b),g(c),d,a) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(b), x1 -> a, x2 -> d, x3 -> g(c)}
% 2.21/0.97 === Backtracking. Learning clause 67:1:0:[7.2,50.1]:: p(g(b),a,d,g(c)) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> d, x1 -> g(c), x2 -> f(g(b)), x3 -> a}
% 2.21/0.97 === Backtracking. Learning clause 68:1:0:[15.2,50.1]:: p(d,g(c),f(g(b)),a) ->
% 2.21/0.97 === Conflict found: 8:2:4:[2.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,x2,x1,f(x0)) {x0 -> g(b), x1 -> f(g(c)), x2 -> d, x3 -> a}
% 2.21/0.97 === Backtracking. Learning clause 69:1:0:[8.2,51.1,15.2]:: p(a,g(b),f(g(c)),d) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(c), x1 -> f(g(d)), x2 -> a, x3 -> b}
% 2.21/0.97 === Backtracking. Learning clause 70:1:0:[7.2,56.1]:: p(g(c),f(g(d)),a,b) ->
% 2.21/0.97 === Backtracking. Learning clause 71:1:0:[2.2,56.1]:: p(a,f(g(d)),f(g(c)),b) ->
% 2.21/0.97 === Backtracking. Learning clause 72:1:0:[2.2,57.1]:: p(c,f(g(b)),f(g(a)),d) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> c, x1 -> d, x2 -> f(g(a)), x3 -> f(g(b))}
% 2.21/0.97 === Backtracking. Learning clause 73:1:0:[15.2,57.1]:: p(c,d,f(g(a)),f(g(b))) ->
% 2.21/0.97 === Backtracking. Learning clause 74:1:0:[2.2,44.1]:: p(a,f(g(b)),f(g(c)),d) ->
% 2.21/0.97 === Backtracking. Learning clause 75:1:0:[3.2,40.1]:: p(g(a),b,f(g(c)),d) ->
% 2.21/0.97 === Backtracking. Learning clause 76:1:0:[2.2,58.1]:: p(d,f(g(c)),g(b),g(a)) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(a), x1 -> g(d), x2 -> c, x3 -> g(b)}
% 2.21/0.97 === Backtracking. Learning clause 77:1:0:[7.2,60.1]:: p(g(a),g(d),c,g(b)) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> c, x1 -> g(b), x2 -> f(g(a)), x3 -> g(d)}
% 2.21/0.97 === Backtracking. Learning clause 78:1:0:[15.2,60.1]:: p(c,g(b),f(g(a)),g(d)) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 127
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Backtracking. Learning clause 79:1:0:[1.2,67.1]:: p(a,d,g(c),g(b)) ->
% 2.21/0.97 === Backtracking. Learning clause 80:1:0:[3.2,47.1]:: p(b,g(c),g(d),a) ->
% 2.21/0.97 === Backtracking. Learning clause 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1)
% 2.21/0.97 === Backtracking. Learning clause 82:1:0:[2.2,75.1,81.2]:: p(d,g(a),b,f(g(c))) ->
% 2.21/0.97 === Backtracking. Learning clause 83:1:0:[1.2,64.1,81.2]:: p(d,g(a),g(b),g(c)) ->
% 2.21/0.97 === Backtracking. Learning clause 84:1:0:[3.2,64.1]:: p(g(a),d,g(c),b) ->
% 2.21/0.97 === Backtracking. Learning clause 85:1:0:[2.2,41.1]:: p(a,b,f(g(c)),g(d)) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> a, x1 -> b, x2 -> f(g(c)), x3 -> f(g(d))}
% 2.21/0.97 === Backtracking. Learning clause 86:1:0:[81.2,71.1]:: p(a,b,f(g(c)),f(g(d))) ->
% 2.21/0.97 === Conflict found: 8:2:4:[2.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,x2,x1,f(x0)) {x0 -> g(b), x1 -> f(g(a)), x2 -> d, x3 -> c}
% 2.21/0.97 === Backtracking. Learning clause 87:1:0:[8.2,73.1,15.2]:: p(c,g(b),f(g(a)),d) ->
% 2.21/0.97 === Conflict found: 8:2:4:[2.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,x2,x1,f(x0)) {x0 -> g(c), x1 -> f(g(d)), x2 -> g(a), x3 -> b}
% 2.21/0.97 === Backtracking. Learning clause 88:1:0:[8.2,46.1]:: p(g(c),f(g(d)),g(a),b) ->
% 2.21/0.97 === Conflict found: 7:2:4:[1.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,f(x0),x1,x2) {x0 -> g(b), x1 -> f(g(a)), x2 -> d, x3 -> g(c)}
% 2.21/0.97 === Backtracking. Learning clause 89:1:0:[7.2,26.1]:: p(g(b),f(g(a)),d,g(c)) ->
% 2.21/0.97 === Conflict found: 8:2:4:[2.1,4.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x3,x2,x1,f(x0)) {x0 -> g(c), x1 -> f(g(d)), x2 -> f(g(a)), x3 -> g(b)}
% 2.21/0.97 === Backtracking. Learning clause 90:1:0:[8.2,19.1,2.2]:: p(g(b),f(g(a)),f(g(d)),g(c)) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 174
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> b, x1 -> a, x2 -> g(d), x3 -> g(c)}
% 2.21/0.97 === Backtracking. Learning clause 91:1:0:[81.2,80.1,1.2,81.2]:: p(a,b,g(c),g(d)) ->
% 2.21/0.97 === Backtracking. Learning clause 92:2:4:[2.2,15.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x2,x1,x0,x3)
% 2.21/0.97 === Backtracking. Learning clause 93:1:0:[3.2,67.1]:: p(g(b),a,d,c) ->
% 2.21/0.97 === Backtracking. Learning clause 94:1:0:[3.2,85.1]:: p(a,b,f(g(c)),d) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> c, x1 -> d, x2 -> f(g(a)), x3 -> g(b)}
% 2.21/0.97 === Backtracking. Learning clause 95:1:0:[81.2,87.1]:: p(c,d,f(g(a)),g(b)) ->
% 2.21/0.97 === Backtracking. Learning clause 96:1:0:[3.2,83.1]:: p(d,g(a),g(b),c) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> d, x1 -> a, x2 -> f(g(b)), x3 -> g(c)}
% 2.21/0.97 === Backtracking. Learning clause 97:1:0:[81.2,68.1,1.2,81.2]:: p(a,d,g(c),f(g(b))) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> g(a), x1 -> g(b), x2 -> c, x3 -> g(d)}
% 2.21/0.97 === Backtracking. Learning clause 98:1:0:[81.2,77.1]:: p(g(a),g(b),c,g(d)) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> g(c), x1 -> b, x2 -> a, x3 -> f(g(d))}
% 2.21/0.97 === Backtracking. Learning clause 99:1:0:[81.2,70.1,1.2]:: p(b,a,f(g(d)),g(c)) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> g(a), x1 -> g(b), x2 -> g(c), x3 -> g(d)}
% 2.21/0.97 === Backtracking. Learning clause 100:1:0:[81.2,30.1]:: p(g(a),g(b),g(c),g(d)) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> g(c), x1 -> b, x2 -> g(a), x3 -> f(g(d))}
% 2.21/0.97 === Backtracking. Learning clause 101:1:0:[81.2,88.1,1.2]:: p(b,g(a),f(g(d)),g(c)) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> g(b), x1 -> g(c), x2 -> g(d), x3 -> f(g(a))}
% 2.21/0.97 === Backtracking. Learning clause 102:1:0:[81.2,25.1]:: p(g(b),g(c),g(d),f(g(a))) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> g(a), x1 -> g(d), x2 -> f(g(c)), x3 -> f(g(b))}
% 2.21/0.97 === Backtracking. Learning clause 103:1:0:[81.2,12.1]:: p(g(a),g(d),f(g(c)),f(g(b))) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> g(a), x1 -> g(b), x2 -> f(g(c)), x3 -> f(g(d))}
% 2.21/0.97 === Backtracking. Learning clause 104:1:0:[81.2,16.1]:: p(g(a),g(b),f(g(c)),f(g(d))) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> g(c), x1 -> g(d), x2 -> f(g(a)), x3 -> f(g(b))}
% 2.21/0.97 === Backtracking. Learning clause 105:1:0:[81.2,17.1]:: p(g(c),g(d),f(g(a)),f(g(b))) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 196
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Conflict found: 92:2:4:[2.2,15.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x2,x1,x0,x3) {x0 -> a, x1 -> b, x2 -> g(c), x3 -> d}
% 2.21/0.97 === Backtracking. Learning clause 106:1:0:[92.2,62.1]:: p(a,b,g(c),d) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> b, x1 -> c, x2 -> g(d), x3 -> g(a)}
% 2.21/0.97 === Backtracking. Learning clause 107:1:0:[81.2,63.1]:: p(b,c,g(d),g(a)) ->
% 2.21/0.97 === Backtracking. Learning clause 108:1:0:[2.2,96.1,81.2]:: p(c,d,g(a),g(b)) ->
% 2.21/0.97 === Backtracking. Learning clause 109:1:0:[1.2,99.1]:: p(a,f(g(d)),g(c),b) ->
% 2.21/0.97 === Backtracking. Learning clause 110:1:0:[3.2,95.1]:: p(c,d,f(g(a)),b) ->
% 2.21/0.97 === Conflict found: 92:2:4:[2.2,15.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x2,x1,x0,x3) {x0 -> b, x1 -> g(a), x2 -> d, x3 -> f(g(c))}
% 2.21/0.97 === Backtracking. Learning clause 111:1:0:[92.2,82.1]:: p(b,g(a),d,f(g(c))) ->
% 2.21/0.97 === Conflict found: 92:2:4:[2.2,15.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x2,x1,x0,x3) {x0 -> c, x1 -> g(b), x2 -> g(a), x3 -> g(d)}
% 2.21/0.97 === Backtracking. Learning clause 112:1:0:[92.2,98.1]:: p(c,g(b),g(a),g(d)) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> b, x1 -> g(a), x2 -> g(d), x3 -> f(g(c))}
% 2.21/0.97 === Backtracking. Learning clause 113:1:0:[81.2,52.1]:: p(b,g(a),g(d),f(g(c))) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> d, x1 -> c, x2 -> f(g(b)), x3 -> f(g(a))}
% 2.21/0.97 === Backtracking. Learning clause 114:1:0:[15.1,8.2,72.1,15.2]:: p(d,g(a),f(g(b)),c) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> d, x1 -> g(a), x2 -> g(b), x3 -> f(g(c))}
% 2.21/0.97 === Backtracking. Learning clause 115:1:0:[81.2,76.1]:: p(d,g(a),g(b),f(g(c))) ->
% 2.21/0.97 === Conflict found: 15:2:4:[1.1,1.2,1.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x1,x2,x3,x0) {x0 -> g(b), x1 -> a, x2 -> g(d), x3 -> f(g(c))}
% 2.21/0.97 === Backtracking. Learning clause 116:1:0:[15.1,8.2,39.1]:: p(g(c),g(d),a,g(b)) ->
% 2.21/0.97 === Conflict found: 92:2:4:[2.2,15.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x2,x1,x0,x3) {x0 -> d, x1 -> f(g(a)), x2 -> g(b), x3 -> g(c)}
% 2.21/0.97 === Backtracking. Learning clause 117:1:0:[92.2,89.1]:: p(d,f(g(a)),g(b),g(c)) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> g(b), x1 -> g(c), x2 -> f(g(d)), x3 -> f(g(a))}
% 2.21/0.97 === Backtracking. Learning clause 118:1:0:[81.2,90.1,8.2]:: p(g(a),f(g(d)),g(c),g(b)) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> g(b), x1 -> g(c), x2 -> f(g(d)), x3 -> f(g(a))}
% 2.21/0.97 === Backtracking. Learning clause 119:1:0:[81.2,90.1]:: p(g(b),g(c),f(g(d)),f(g(a))) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 216
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Conflict found: 92:2:4:[2.2,15.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x2,x1,x0,x3) {x0 -> d, x1 -> a, x2 -> g(b), x3 -> c}
% 2.21/0.97 === Backtracking. Learning clause 120:1:0:[92.2,93.1,15.2,92.2]:: p(a,d,c,g(b)) ->
% 2.21/0.97 === Backtracking. Learning clause 121:1:0:[3.2,107.1]:: p(b,c,g(d),a) ->
% 2.21/0.97 === Backtracking. Learning clause 122:1:0:[2.2,110.1,81.2]:: p(b,c,d,f(g(a))) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> d, x1 -> c, x2 -> f(g(b)), x3 -> g(a)}
% 2.21/0.97 === Backtracking. Learning clause 123:1:0:[81.2,114.1,1.2,81.2]:: p(c,d,g(a),f(g(b))) ->
% 2.21/0.97 === Backtracking. Learning clause 124:1:0:[3.2,101.1]:: p(b,g(a),f(g(d)),c) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> g(a), x1 -> g(b), x2 -> g(c), x3 -> f(g(d))}
% 2.21/0.97 === Backtracking. Learning clause 125:1:0:[81.2,118.1]:: p(g(a),g(b),g(c),f(g(d))) ->
% 2.21/0.97 === Backtracking. Learning clause 126:1:0:[3.2,90.1]:: p(g(b),f(g(a)),f(g(d)),c) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 227
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Backtracking. Learning clause 127:1:0:[3.2,120.1]:: p(a,d,c,b) ->
% 2.21/0.97 === Backtracking. Learning clause 128:1:0:[1.2,84.1,92.2,81.2]:: p(b,g(a),d,g(c)) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> a, x1 -> d, x2 -> f(g(c)), x3 -> g(b)}
% 2.21/0.97 === Backtracking. Learning clause 129:1:0:[81.2,69.1]:: p(a,d,f(g(c)),g(b)) ->
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> a, x1 -> b, x2 -> g(c), x3 -> f(g(d))}
% 2.21/0.97 === Backtracking. Learning clause 130:1:0:[81.2,109.1]:: p(a,b,g(c),f(g(d))) ->
% 2.21/0.97 === Conflict found: 92:2:4:[2.2,15.1]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x2,x1,x0,x3) {x0 -> a, x1 -> g(d), x2 -> g(c), x3 -> g(b)}
% 2.21/0.97 === Backtracking. Learning clause 131:1:0:[92.2,116.1]:: p(a,g(d),g(c),g(b)) ->
% 2.21/0.97 === Backtracking. Learning clause 132:1:0:[2.2,126.1,81.2]:: p(c,g(b),f(g(a)),f(g(d))) ->
% 2.21/0.97 === Clause set with instances from active satisfied. Growing active. New size: 232
% 2.21/0.97 === Restarting.
% 2.21/0.97 === Conflict found: 81:2:4:[2.1,15.2]:TopTopTopTop: p(x0,x1,x2,x3) -> p(x0,x3,x2,x1) {x0 -> a, x1 -> b, x2 -> c, x3 -> d}
% 2.21/0.97
% 2.21/0.97 SZS status Unsatisfiable
% 2.21/0.97
% 2.21/0.97 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.21/0.97
% 2.21/0.97 SPASS-SCL-FOL Statistics:
% 2.21/0.97 Number of learned clauses: 126
% 2.21/0.97 Number of propagations: 6422
% 2.21/0.97 Number of decisions: 1445
% 2.21/0.97 Number of resolutions: 156
% 2.21/0.97 Number of condensations: 0
% 2.21/0.97 Number of sub resolutions: 0
% 2.21/0.97 Number of input literals (deduplicated): 5
% 2.21/0.97 Number of grows: 13
% 2.21/0.97 Number of considered ground atoms: 232
% 2.21/0.97
% 2.21/0.97 Needed: 0:00:00.41
% 2.21/0.97
%------------------------------------------------------------------------------