%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : COM003-1 : TPTP v9.2.1. Bugfixed v1.0.1.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:19:09 PM UTC 2026
% Result : Unsatisfiable 1.42s 0.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM003-1 : TPTP v9.2.1. Bugfixed v1.0.1.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n009.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 11:35:26 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83 Execution resolution_2 ended with status: unsatisfiable
% 1.42/0.83 Used heuristic: resolution_2
% 1.42/0.83
% 1.42/0.83 Input Clauses:
% 1.42/0.83
% 1.42/0.83 Predicates: algorithm program decides halts2 halts3 outputs
% 1.42/0.83 Fol Constants: c1 good bad c2 c3 c4
% 1.42/0.83 Fol Functions: f2 f1 f4 f3 f5 f6
% 1.42/0.83 Problem Properties:
% 1.42/0.83 This is a full first-order problem without equality.
% 1.42/0.83
% 1.42/0.83 After reduction: Problem Properties:
% 1.42/0.83 This is a full first-order problem without equality.
% 1.42/0.83
% 1.42/0.83
% 1.42/0.83 Reduced Input Clauses:
% 1.42/0.83 51:4:3:[7.3,5.2]:TopTopTop: program(x0),program(x1) -> program(f4(x0)),halts3(x0,x1,x2)
% 1.42/0.83 52:4:3:[11.3,9.3]:TopTopTop: program(x0),decides(x0,f4(x0),f3(x0)),program(x1) -> halts3(x0,x1,x2)
% 1.42/0.83 53:4:2:[16.3,14.2]:TopTop: program(x0),program(x1) -> program(f5(x0)),halts2(c2,x1)
% 1.42/0.83 54:6:2:[21.5,19.4]:TopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,bad),program(x1) -> halts2(f5(x0),f5(x0)),halts2(c2,x1)
% 1.42/0.83 55:6:2:[26.5,24.5]:TopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),halts2(f5(x0),f5(x0)),program(x1) -> halts2(c2,x1)
% 1.42/0.83 56:6:2:[31.5,29.5]:TopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),outputs(x0,bad),program(x1) -> halts2(c2,x1)
% 1.42/0.83
% 1.42/0.83 Most General Atoms: algorithm(x0) decides(c1,x1,x2) decides(x0,f2(x0),f1(x0)) program(x0) halts3(x0,x1,x2) halts2(x1,x2) outputs(x0,good) outputs(x0,bad) decides(x0,f4(x0),f3(x0)) decides(c4,x0,x1)
% 1.42/0.83
% 1.42/0.83 === Starting SPASS-SCL-FOL A Little Less Naive, considering 49 atoms initially, heuristics mode: resolution_2 ===
% 1.42/0.83
% 1.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 51
% 1.42/0.83 === Restarting.
% 1.42/0.83 === Backtracking. Learning clause 57:2:0:[3.1,49.1]:: decides(c4,f2(c4),f1(c4)) -> program(c1)
% 1.42/0.83 === Backtracking. Learning clause 58:2:0:[1.1,49.1]:: -> program(f2(c4)),program(c1)
% 1.42/0.83 === Backtracking. Learning clause 60:5:1:[1.2,59.1,2.2,6.4,10.2,41.3]:Top: algorithm(x0),halts2(c1,f6(c1)),halts2(f6(c1),f6(c1)) -> program(f2(x0)),program(c3)
% 1.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 51
% 1.42/0.83 === Restarting.
% 1.42/0.83 === Conflict found: 57:2:0:[3.1,49.1]:: decides(c4,f2(c4),f1(c4)) -> program(c1) {}
% 1.42/0.83 === Backtracking. Learning clause 62:1:0:[58.0,61.0,57.1,50.2]:: -> program(c1)
% 1.42/0.83 === Conflict found: 51:4:3:[7.3,5.2]:TopTopTop: program(x0),program(x1) -> program(f4(x0)),halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 64:6:2:[8.4,63.2,51.2,16.3,31.2]:TopTop: program(x0),outputs(x0,good),program(x1) -> program(f4(x0)),halts2(x1,x1),halts2(c2,x1)
% 1.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 51
% 1.42/0.83 === Restarting.
% 1.42/0.83 === Backtracking. Learning clause 65:3:1:[6.1,62.1]:Top: halts2(c1,x0) -> program(f4(c1)),outputs(c1,good)
% 1.42/0.83 === Conflict found: 52:4:3:[11.3,9.3]:TopTopTop: program(x0),decides(x0,f4(x0),f3(x0)),program(x1) -> halts3(x0,x1,x2) {x0 -> c1, x1 -> c1, x2 -> c1}
% 1.42/0.83 === Backtracking. Learning clause 66:2:1:[52.1,62.1]:Top: decides(c1,f4(c1),f3(c1)) -> halts3(c1,c1,x0)
% 1.42/0.83 === Conflict found: 51:4:3:[7.3,5.2]:TopTopTop: program(x0),program(x1) -> program(f4(x0)),halts3(x0,x1,x2) {x0 -> c1, x1 -> c1, x2 -> c1}
% 1.42/0.83 === Backtracking. Learning clause 67:2:1:[51.1,62.1]:Top: -> program(f4(c1)),halts3(c1,c1,x0)
% 1.42/0.83 === Backtracking. Learning clause 68:3:2:[4.3,62.1]:TopTop: algorithm(x0),decides(x0,f2(x0),f1(x0)) -> decides(c1,c1,x1)
% 1.42/0.83 === Backtracking. Learning clause 69:2:0:[33.1,62.1]:: -> program(f6(c1)),program(c3)
% 1.42/0.83 === Backtracking. Learning clause 70:2:0:[13.1,62.1]:: -> program(f5(c1)),program(c2)
% 1.42/0.83 === Backtracking. Learning clause 71:1:1:[50.1,62.1]:Top: -> decides(c4,c1,x0)
% 1.42/0.83 === Backtracking. Learning clause 73:6:3:[13.1,72.0,12.5,28.4,23.4,10.5]:TopTopTop: halts3(x0,f5(x0),f5(x0)),program(x0),decides(x0,f4(x0),f3(x0)),program(x1),halts2(x1,x2) -> program(c2)
% 1.42/0.83 === Backtracking. Learning clause 75:2:0:[62.0,74.0,18.4,73.5,12.5,73.5,52.4,70.1]:: decides(c1,f4(c1),f3(c1)) -> program(c2)
% 1.42/0.83 === Backtracking. Learning clause 77:6:1:[62.0,76.2,12.4,41.4,69.1]:Top: program(x0),decides(x0,f4(x0),f3(x0)),halts2(c1,f6(c1)),outputs(c1,good) -> outputs(x0,bad),program(c3)
% 1.42/0.83 === Backtracking. Learning clause 78:8:2:[12.4,42.4,34.5,12.4,12.4,77.6]:TopTop: halts2(x0,f6(x0)),outputs(x0,good),program(x0),program(x1),decides(x1,f4(x1),f3(x1)),halts2(c1,f6(c1)),outputs(c1,good) -> outputs(x1,bad)
% 1.42/0.83 === Backtracking. Learning clause 80:2:2:[49.0,79.0,50.1,2.3,4.2]:TopTop: program(x0) -> decides(c1,x0,x1)
% 1.42/0.83 === Conflict found: 80:2:2:[49.0,79.0,50.1,2.3,4.2]:TopTop: program(x0) -> decides(c1,x0,x1) {x0 -> f4(c1), x1 -> f3(c1)}
% 1.42/0.83 === Backtracking. Learning clause 82:3:2:[62.0,81.0,80.1,8.3,12.2]:TopTop: program(x0) -> halts2(x0,x1),outputs(c1,bad)
% 1.42/0.83 === Backtracking. Learning clause 83:3:2:[34.4,82.2,82.2,33.3,82.1]:TopTop: program(x0) -> halts2(f6(x0),x1),outputs(c1,bad)
% 1.42/0.83 === Conflict found: 80:2:2:[49.0,79.0,50.1,2.3,4.2]:TopTop: program(x0) -> decides(c1,x0,x1) {x0 -> f4(c1), x1 -> f3(c1)}
% 1.42/0.83 === Backtracking. Learning clause 85:3:0:[62.0,84.1,80.1,6.4,10.2,41.3,82.2,69.1]:: halts2(f6(c1),f6(c1)) -> outputs(c1,bad),program(c3)
% 1.42/0.83 === Backtracking. Learning clause 87:3:1:[33.2,86.1,34.4,82.2,82.2]:Top: program(x0) -> program(f6(x0)),outputs(c1,bad)
% 1.42/0.83 === Conflict found: 80:2:2:[49.0,79.0,50.1,2.3,4.2]:TopTop: program(x0) -> decides(c1,x0,x1) {x0 -> f4(c1), x1 -> f3(c1)}
% 1.42/0.83 === Backtracking. Learning clause 89:1:0:[62.0,88.0,80.1,6.4,10.2,42.3,82.2,82.2,82.2,85.3,83.2]:: -> outputs(c1,bad)
% 1.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 51
% 1.42/0.83 === Restarting.
% 1.42/0.83 === Backtracking. Learning clause 91:5:1:[62.0,90.0,30.4,89.1]:Top: halts3(c1,f5(c1),f5(c1)),outputs(c1,good),program(x0),halts2(x0,x0) -> outputs(c2,good)
% 1.42/0.83 === Conflict found: 56:6:2:[31.5,29.5]:TopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),outputs(x0,bad),program(x1) -> halts2(c2,x1) {x0 -> c1, x1 -> c1}
% 1.42/0.83 === Backtracking. Learning clause 93:4:1:[62.0,92.0,56.4,89.1]:Top: halts3(c1,f5(c1),f5(c1)),outputs(c1,good),program(x0) -> halts2(c2,x0)
% 1.42/0.83 === Backtracking. Learning clause 95:3:0:[62.0,94.0,45.4,89.1]:: halts2(c1,f6(c1)),outputs(c1,good) -> program(c3)
% 1.42/0.83 === Backtracking. Learning clause 97:3:0:[62.0,96.0,37.3,89.1]:: halts2(c1,f6(c1)) -> halts2(f6(c1),f6(c1)),program(c3)
% 1.42/0.83 === Backtracking. Learning clause 99:3:0:[62.0,98.0,18.3,89.1]:: halts3(c1,f5(c1),f5(c1)) -> halts2(f5(c1),f5(c1)),program(c2)
% 1.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 115
% 1.42/0.83 === Conflict found: 53:4:2:[16.3,14.2]:TopTop: program(x0),program(x1) -> program(f5(x0)),halts2(c2,x1) {x0 -> c1, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 102:7:2:[15.4,100.1,13.2,101.6,53.4,46.2,33.2]:TopTop: program(x0),outputs(c2,bad),program(x1),halts2(x1,x1),halts2(c3,x1) -> program(f5(x0)),program(c3)
% 1.42/0.83 === Conflict found: 56:6:2:[31.5,29.5]:TopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),outputs(x0,bad),program(x1) -> halts2(c2,x1) {x0 -> c1, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 104:14:4:[18.4,103.0,56.5,33.2,46.2,32.7,20.7]:TopTopTopTop: program(x0),halts2(x0,x0),halts2(c3,x0),program(x1),halts3(x1,f5(x1),f5(x1)),outputs(x1,good),outputs(x1,bad),program(x2),program(x3),halts3(x3,f5(x3),f5(x3)),outputs(x3,bad) -> program(c3),halts2(x2,x2),halts2(f5(x3),f5(x3))
% 1.42/0.83 === Backtracking. Learning clause 106:13:4:[18.4,105.10,45.4,32.7,20.7,56.6,33.2]:TopTopTopTop: program(x0),program(x1),halts3(x1,f5(x1),f5(x1)),outputs(x1,bad),program(x2),halts2(x2,x2),program(x3),halts3(x3,f5(x3),f5(x3)),outputs(x3,good),outputs(x3,bad) -> halts2(x0,x0),halts2(f5(x1),f5(x1)),program(c3)
% 1.42/0.83 === Backtracking. Learning clause 108:11:3:[18.4,107.8,37.4,106.6,32.7,56.6,33.2]:TopTopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,bad),program(x1),program(x2),halts3(x2,f5(x2),f5(x2)),outputs(x2,good),outputs(x2,bad) -> halts2(f5(x0),f5(x0)),halts2(x1,x1),program(c3)
% 1.42/0.83 === Backtracking. Learning clause 111:14:4:[108.9,109.4,33.1,110.9,42.4,108.10]:TopTopTopTop: program(x0),halts2(x0,f6(x0)),outputs(x0,good),program(x1),halts2(c3,x1),program(x2),halts3(x2,f5(x2),f5(x2)),outputs(x2,bad),program(x3),halts3(x3,f5(x3),f5(x3)),outputs(x3,good),outputs(x3,bad) -> halts2(f5(x2),f5(x2)),program(c3)
% 1.42/0.83 === Backtracking. Learning clause 113:11:2:[18.4,112.9,41.4,108.10,91.5,108.10,56.6,33.2]:TopTop: halts3(c1,f5(c1),f5(c1)),outputs(c1,good),program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,bad),program(x1),halts3(x1,f5(x1),f5(x1)),outputs(x1,good),outputs(x1,bad) -> halts2(f5(x0),f5(x0)),program(c3)
% 1.42/0.83 === Backtracking. Learning clause 114:4:0:[33.1,99.3]:: halts3(c1,f5(c1),f5(c1)) -> program(f6(c2)),program(c3),halts2(f5(c1),f5(c1))
% 1.42/0.83 === Backtracking. Learning clause 117:7:1:[18.4,115.0,54.5,116.1,37.3,22.7,20.5]:Top: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,bad),program(f6(c2)) -> program(c3),halts2(f5(x0),f5(x0)),outputs(c2,good)
% 1.42/0.83 === Backtracking. Learning clause 118:6:0:[41.1,99.3]:: halts2(c2,f6(c2)),outputs(c2,good),halts2(f6(c2),f6(c2)),halts3(c1,f5(c1),f5(c1)) -> program(c3),halts2(f5(c1),f5(c1))
% 1.42/0.83 === Backtracking. Learning clause 119:7:1:[37.1,99.3,22.7,118.3,54.6,117.7,114.2]:Top: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,bad),halts3(c1,f5(c1),f5(c1)) -> halts2(f5(x0),f5(x0)),program(c3),halts2(f5(c1),f5(c1))
% 1.42/0.83 === Backtracking. Learning clause 120:6:1:[22.6,20.5]:Top: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,bad) -> outputs(c2,bad),halts2(f5(x0),f5(x0)),outputs(c2,good)
% 1.42/0.83 === Backtracking. Learning clause 122:6:2:[33.2,121.5,47.6,34.3]:TopTop: program(x0),halts2(x0,f6(x0)),outputs(x0,good),outputs(x0,bad),program(x1) -> program(f6(x1))
% 1.42/0.83 === Backtracking. Learning clause 123:7:1:[35.4,34.3,119.6,99.3]:Top: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,bad),halts3(c1,f5(c1),f5(c1)) -> program(f6(c2)),halts2(f5(x0),f5(x0)),halts2(f5(c1),f5(c1))
% 1.42/0.83 === Backtracking. Learning clause 125:9:2:[18.4,124.0,42.6,43.6,20.7]:TopTop: halts2(c2,f6(c2)),halts2(f6(c2),f6(c2)),program(c3),program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,bad),program(x1),halts2(x1,x1) -> halts2(f5(x0),f5(x0))
% 1.42/0.83 === Backtracking. Learning clause 127:9:2:[37.4,126.6,20.5,39.6]:TopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,bad),program(x1),halts2(x1,f6(x1)),outputs(x1,bad) -> halts2(f5(x0),f5(x0)),outputs(c2,good),halts2(f6(x1),f6(x1))
% 1.42/0.83 === Backtracking. Learning clause 129:2:0:[62.0,128.0,38.5,39.6,22.7,125.2,54.6,119.6,99.3,123.5,89.1]:: halts3(c1,f5(c1),f5(c1)) -> halts2(f5(c1),f5(c1))
% 1.42/0.83 === Conflict found: 80:2:2:[49.0,79.0,50.1,2.3,4.2]:TopTop: program(x0) -> decides(c1,x0,x1) {x0 -> f4(c1), x1 -> f3(c1)}
% 1.42/0.83 === Backtracking. Learning clause 131:4:2:[62.0,130.0,80.1,6.4,75.1]:TopTop: program(x0),halts2(x0,x1) -> outputs(c1,good),program(c2)
% 1.42/0.83 === Conflict found: 131:4:2:[62.0,130.0,80.1,6.4,75.1]:TopTop: program(x0),halts2(x0,x1) -> outputs(c1,good),program(c2) {x0 -> f5(c1), x1 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 134:2:0:[62.0,132.0,89.0,133.2,131.1,70.1,129.2,28.3]:: halts3(c1,f5(c1),f5(c1)) -> program(c2)
% 1.42/0.83 === Backtracking. Learning clause 135:2:1:[34.3,35.4,33.3]:Top: program(x0) -> program(f6(x0))
% 1.42/0.83 === Backtracking. Learning clause 138:3:0:[62.0,136.0,70.0,137.1,7.5,134.1]:: -> program(f4(c1)),halts2(f5(c1),f5(c1)),program(c2)
% 1.42/0.83 === Conflict found: 51:4:3:[7.3,5.2]:TopTopTop: program(x0),program(x1) -> program(f4(x0)),halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 140:1:0:[62.0,139.0,51.4,134.1,70.1,80.1,75.1,135.1]:: -> program(f6(c2))
% 1.42/0.83 === Conflict found: 51:4:3:[7.3,5.2]:TopTopTop: program(x0),program(x1) -> program(f4(x0)),halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 141:1:0:[51.1,62.1,134.1,70.1,80.1,75.1]:: -> program(c2)
% 1.42/0.83 === Backtracking. Learning clause 142:4:2:[6.1,62.1]:TopTop: program(x0),halts2(x0,x1) -> program(f4(c1)),outputs(c1,good)
% 1.42/0.83 === Backtracking. Learning clause 145:5:2:[89.0,143.0,140.0,144.1,25.3,142.4,117.6,51.4,15.4,62.1,80.1]:TopTop: program(x0),halts2(x0,x0) -> program(c3),outputs(c2,good),decides(c1,f4(c1),x1)
% 1.42/0.83 === Backtracking. Learning clause 148:4:1:[89.0,146.0,140.0,147.1,25.3,10.5,117.6,52.4,15.4,62.1,145.5]:Top: program(x0),halts2(x0,x0) -> program(c3),outputs(c2,good)
% 1.42/0.83 === Conflict found: 53:4:2:[16.3,14.2]:TopTop: program(x0),program(x1) -> program(f5(x0)),halts2(c2,x1) {x0 -> c1, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 151:5:1:[140.0,149.1,13.2,150.2,53.4,41.2]:Top: program(x0),outputs(c2,good),halts2(f6(c2),f6(c2)) -> program(f5(x0)),program(c3)
% 1.42/0.83 === Conflict found: 55:6:2:[26.5,24.5]:TopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),halts2(f5(x0),f5(x0)),program(x1) -> halts2(c2,x1) {x0 -> c1, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 153:6:4:[62.0,152.3,55.3,6.5,129.2,51.4,80.1]:TopTopTopTop: program(x0),program(x1),halts2(x1,x2),program(f5(c1)) -> halts2(c2,x0),decides(c1,f4(c1),x3)
% 1.42/0.83 === Conflict found: 55:6:2:[26.5,24.5]:TopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),halts2(f5(x0),f5(x0)),program(x1) -> halts2(c2,x1) {x0 -> c1, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 156:2:0:[140.0,154.0,141.0,155.1,55.3,10.5,129.2,52.4,153.6,41.2,151.4,148.4,62.1]:: halts2(f6(c2),f6(c2)) -> program(c3)
% 1.42/0.83 === Backtracking. Learning clause 159:3:0:[70.1,157.0,140.0,158.2,43.5,156.2,15.5,53.4,62.1]:: halts2(f6(c2),f6(c2)) -> halts2(c3,c3),program(f5(c1))
% 1.42/0.83 === Backtracking. Learning clause 161:6:2:[62.0,160.0,6.4,80.1,91.2,129.2]:TopTop: program(f5(c1)),program(x0),halts2(x0,x0),halts3(c1,f5(c1),f5(c1)) -> decides(c1,f4(c1),x1),outputs(c2,good)
% 1.42/0.83 === Backtracking. Learning clause 162:5:4:[7.3,80.1]:TopTopTopTop: program(x0),program(x1) -> halts2(x1,x2),halts3(x0,x1,x2),decides(c1,f4(x0),x3)
% 1.42/0.83 === Conflict found: 129:2:0:[62.0,128.0,38.5,39.6,22.7,125.2,54.6,119.6,99.3,123.5,89.1]:: halts3(c1,f5(c1),f5(c1)) -> halts2(f5(c1),f5(c1)) {}
% 1.42/0.83 === Backtracking. Learning clause 164:3:1:[62.0,163.0,129.1,162.4]:Top: program(f5(c1)) -> halts2(f5(c1),f5(c1)),decides(c1,f4(c1),x0)
% 1.42/0.83 === Backtracking. Learning clause 168:4:1:[134.1,165.0,140.0,166.3,159.2,167.4,43.5,156.2,161.6,153.5]:Top: halts2(f6(c2),f6(c2)),halts3(c1,f5(c1),f5(c1)) -> halts2(c3,c3),decides(c1,f4(c1),x0)
% 1.42/0.83 === Conflict found: 51:4:3:[7.3,5.2]:TopTopTop: program(x0),program(x1) -> program(f4(x0)),halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 171:3:1:[62.0,169.0,159.2,170.1,51.3,80.1,168.2]:Top: halts2(f6(c2),f6(c2)) -> halts2(c3,c3),decides(c1,f4(c1),x0)
% 1.42/0.83 === Backtracking. Learning clause 174:4:0:[134.1,172.0,140.0,173.3,43.5,156.2,91.5,93.4,142.4]:: halts2(f6(c2),f6(c2)),halts3(c1,f5(c1),f5(c1)) -> halts2(c3,c3),program(f4(c1))
% 1.42/0.83 === Backtracking. Learning clause 176:9:2:[75.1,175.4,10.1,62.1,91.2,43.3]:TopTop: decides(c1,f4(c1),f3(c1)),halts3(c1,f5(c1),f5(c1)),program(x0),halts2(x0,x0),halts2(c2,f6(c2)),halts2(f6(c2),f6(c2)),program(x1) -> halts2(x1,x1),halts2(c3,x1)
% 1.42/0.83 === Backtracking. Learning clause 178:3:0:[140.0,177.0,10.1,62.1,93.2,176.5,171.3,156.2]:: halts3(c1,f5(c1),f5(c1)),halts2(f6(c2),f6(c2)) -> halts2(c3,c3)
% 1.42/0.83 === Backtracking. Learning clause 179:6:2:[7.2,159.3]:TopTop: program(x0),halts2(f6(c2),f6(c2)) -> program(f4(x0)),halts2(f5(c1),x1),halts3(x0,f5(c1),x1),halts2(c3,c3)
% 1.42/0.83 === Conflict found: 51:4:3:[7.3,5.2]:TopTopTop: program(x0),program(x1) -> program(f4(x0)),halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 180:5:2:[51.2,159.3]:TopTop: program(x0),halts2(f6(c2),f6(c2)) -> program(f4(x0)),halts3(x0,f5(c1),x1),halts2(c3,c3)
% 1.42/0.83 === Conflict found: 52:4:3:[11.3,9.3]:TopTopTop: program(x0),decides(x0,f4(x0),f3(x0)),program(x1) -> halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 181:2:0:[52.3,159.3,62.1,171.3,178.1]:: halts2(f6(c2),f6(c2)) -> halts2(c3,c3)
% 1.42/0.83 === Backtracking. Learning clause 184:5:1:[140.0,182.1,13.2,183.2,17.5,37.3,181.1]:Top: program(x0),halts2(c2,f6(c2)) -> program(f5(x0)),program(c3),halts2(c3,c3)
% 1.42/0.83 === Backtracking. Learning clause 187:3:1:[13.2,185.0,140.0,186.2,39.3,17.5,181.1,184.4,53.4]:Top: program(x0) -> halts2(c3,c3),program(f5(x0))
% 1.42/0.83 === Conflict found: 184:5:1:[140.0,182.1,13.2,183.2,17.5,37.3,181.1]:Top: program(x0),halts2(c2,f6(c2)) -> program(f5(x0)),program(c3),halts2(c3,c3) {x0 -> c1}
% 1.42/0.83 === Backtracking. Learning clause 188:4:0:[184.1,62.1]:: halts2(c2,f6(c2)) -> program(f5(c1)),program(c3),halts2(c3,c3)
% 1.42/0.83 === Conflict found: 187:3:1:[13.2,185.0,140.0,186.2,39.3,17.5,181.1,184.4,53.4]:Top: program(x0) -> halts2(c3,c3),program(f5(x0)) {x0 -> c1}
% 1.42/0.83 === Backtracking. Learning clause 189:2:0:[187.1,62.1]:: -> halts2(c3,c3),program(f5(c1))
% 1.42/0.83 === Backtracking. Learning clause 193:7:1:[62.0,190.0,129.1,191.2,134.1,192.4,27.7,45.4,142.4]:Top: halts3(c1,f5(c1),f5(c1)),program(x0),halts2(c2,f6(c2)),outputs(c2,good) -> halts2(x0,x0),program(c3),program(f4(c1))
% 1.42/0.83 === Backtracking. Learning clause 198:4:0:[134.1,194.0,62.0,195.1,140.0,196.2,188.1,197.4,27.7,45.4,10.5,80.2,193.7,181.1,148.4,129.2]:: halts2(c2,f6(c2)),halts3(c1,f5(c1),f5(c1)) -> halts2(c3,c3),program(c3)
% 1.42/0.83 === Conflict found: 142:4:2:[6.1,62.1]:TopTop: program(x0),halts2(x0,x1) -> program(f4(c1)),outputs(c1,good) {x0 -> f5(c1), x1 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 199:4:0:[142.2,129.2]:: program(f5(c1)),halts3(c1,f5(c1),f5(c1)) -> program(f4(c1)),outputs(c1,good)
% 1.42/0.83 === Backtracking. Learning clause 203:3:0:[62.0,200.0,189.1,201.1,140.0,202.2,10.2,80.2,129.2,199.3,93.2,198.1]:: halts3(c1,f5(c1),f5(c1)) -> halts2(c3,c3),program(c3)
% 1.42/0.83 === Conflict found: 51:4:3:[7.3,5.2]:TopTopTop: program(x0),program(x1) -> program(f4(x0)),halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 206:3:0:[62.0,204.0,189.1,205.1,51.4,203.1]:: -> program(f4(c1)),halts2(c3,c3),program(c3)
% 1.42/0.83 === Conflict found: 52:4:3:[11.3,9.3]:TopTopTop: program(x0),decides(x0,f4(x0),f3(x0)),program(x1) -> halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 209:2:0:[62.0,207.0,189.1,208.1,52.2,80.2,203.1,206.1]:: -> halts2(c3,c3),program(c3)
% 1.42/0.83 === Backtracking. Learning clause 212:3:0:[134.1,210.0,140.0,211.1,47.4,27.7,91.5,62.1,93.4,142.4,189.2,209.2,129.2]:: halts3(c1,f5(c1),f5(c1)) -> program(f4(c1)),halts2(c3,c3)
% 1.42/0.83 === Backtracking. Learning clause 213:5:2:[11.1,62.1,164.3]:TopTop: program(x0),program(f5(c1)) -> halts2(x0,x1),halts3(c1,x0,x1),halts2(f5(c1),f5(c1))
% 1.42/0.83 === Conflict found: 51:4:3:[7.3,5.2]:TopTopTop: program(x0),program(x1) -> program(f4(x0)),halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 214:2:0:[51.1,62.1,189.2,212.1]:: -> program(f4(c1)),halts2(c3,c3)
% 1.42/0.83 === Backtracking. Learning clause 218:2:0:[134.1,215.0,140.0,216.1,212.1,217.2,47.4,27.7,91.5,55.6,10.5,209.2,80.2,189.2,129.2,62.1]:: halts3(c1,f5(c1),f5(c1)) -> halts2(c3,c3)
% 1.42/0.83 === Conflict found: 52:4:3:[11.3,9.3]:TopTopTop: program(x0),decides(x0,f4(x0),f3(x0)),program(x1) -> halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 219:1:0:[52.2,80.2,189.2,62.1,214.1,218.1]:: -> halts2(c3,c3)
% 1.42/0.83 === Backtracking. Learning clause 220:6:1:[27.5,140.1,156.1]:Top: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),halts2(f5(x0),f5(x0)) -> outputs(c2,bad),program(c3)
% 1.42/0.83 === Backtracking. Learning clause 221:6:1:[37.1,141.1,156.1,220.5]:Top: halts2(c2,f6(c2)),program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),halts2(f5(x0),f5(x0)) -> program(c3)
% 1.42/0.83 === Conflict found: 142:4:2:[6.1,62.1]:TopTop: program(x0),halts2(x0,x1) -> program(f4(c1)),outputs(c1,good) {x0 -> c2, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 224:4:0:[62.0,222.1,129.1,223.3,142.1,141.1,221.4]:: halts2(c2,f6(c2)),halts3(c1,f5(c1),f5(c1)) -> program(f4(c1)),program(c3)
% 1.42/0.83 === Backtracking. Learning clause 225:4:1:[15.2,140.1]:Top: program(x0),halts2(f6(c2),f6(c2)) -> program(f5(x0)),outputs(c2,good)
% 1.42/0.83 === Backtracking. Learning clause 227:4:1:[156.1,226.1,42.6,219.1,141.1,225.4]:Top: halts2(c2,f6(c2)),program(x0),halts2(f6(c2),f6(c2)) -> program(f5(x0))
% 1.42/0.83 === Backtracking. Learning clause 228:6:1:[27.5,140.1]:Top: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),halts2(f5(x0),f5(x0)) -> halts2(f6(c2),f6(c2)),outputs(c2,bad)
% 1.42/0.83 === Backtracking. Learning clause 230:7:2:[221.5,229.0,38.5,219.1,141.1,228.6,227.3]:TopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),halts2(f5(x0),f5(x0)),halts2(c2,f6(c2)),program(x1) -> program(f5(x1))
% 1.42/0.83 === Conflict found: 142:4:2:[6.1,62.1]:TopTop: program(x0),halts2(x0,x1) -> program(f4(c1)),outputs(c1,good) {x0 -> c2, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 233:5:1:[62.0,231.0,129.1,232.2,142.1,141.1,230.3]:Top: halts3(c1,f5(c1),f5(c1)),halts2(c2,f6(c2)),program(x0) -> program(f4(c1)),program(f5(x0))
% 1.42/0.83 === Conflict found: 93:4:1:[62.0,92.0,56.4,89.1]:Top: halts3(c1,f5(c1),f5(c1)),outputs(c1,good),program(x0) -> halts2(c2,x0) {x0 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 234:5:1:[93.3,140.1,233.2]:Top: outputs(c1,good),halts3(c1,f5(c1),f5(c1)),program(x0) -> program(f4(c1)),program(f5(x0))
% 1.42/0.83 === Conflict found: 53:4:2:[16.3,14.2]:TopTop: program(x0),program(x1) -> program(f5(x0)),halts2(c2,x1) {x0 -> c1, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 235:4:1:[53.2,140.1,233.2]:Top: halts3(c1,f5(c1),f5(c1)),program(x0) -> program(f4(c1)),program(f5(x0))
% 1.42/0.83 === Backtracking. Learning clause 238:5:0:[233.4,236.0,62.0,237.1,42.6,219.1,91.5,228.5,129.2,224.4,141.1]:: outputs(c1,good),halts2(c2,f6(c2)),halts3(c1,f5(c1),f5(c1)) -> outputs(c2,bad),program(f4(c1))
% 1.42/0.83 === Backtracking. Learning clause 240:4:1:[41.4,239.4,42.6,219.1]:Top: program(x0),halts2(x0,f6(x0)),outputs(x0,good),halts2(f6(x0),f6(x0)) ->
% 1.42/0.83 === Backtracking. Learning clause 242:4:0:[62.0,241.0,38.5,219.1,240.4,91.5,129.2,224.4,141.1,235.4,238.4]:: outputs(c1,good),halts2(c2,f6(c2)),halts3(c1,f5(c1),f5(c1)) -> program(f4(c1))
% 1.42/0.83 === Conflict found: 55:6:2:[26.5,24.5]:TopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),halts2(f5(x0),f5(x0)),program(x1) -> halts2(c2,x1) {x0 -> c1, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 244:3:0:[62.0,243.0,55.5,140.1,129.2,242.2]:: outputs(c1,good),halts3(c1,f5(c1),f5(c1)) -> program(f4(c1))
% 1.42/0.83 === Conflict found: 199:4:0:[142.2,129.2]:: program(f5(c1)),halts3(c1,f5(c1),f5(c1)) -> program(f4(c1)),outputs(c1,good) {}
% 1.42/0.83 === Backtracking. Learning clause 246:2:0:[62.0,245.0,199.1,235.4,244.1]:: halts3(c1,f5(c1),f5(c1)) -> program(f4(c1))
% 1.42/0.83 === Conflict found: 91:5:1:[62.0,90.0,30.4,89.1]:Top: halts3(c1,f5(c1),f5(c1)),outputs(c1,good),program(x0),halts2(x0,x0) -> outputs(c2,good) {x0 -> c3}
% 1.42/0.83 === Backtracking. Learning clause 248:4:0:[134.1,247.2,91.4,219.1,240.3,156.2]:: halts3(c1,f5(c1),f5(c1)),outputs(c1,good),halts2(c2,f6(c2)),halts2(f6(c2),f6(c2)) ->
% 1.42/0.83 === Conflict found: 220:6:1:[27.5,140.1,156.1]:Top: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),halts2(f5(x0),f5(x0)) -> outputs(c2,bad),program(c3) {x0 -> c1}
% 1.42/0.83 === Backtracking. Learning clause 252:4:0:[129.1,249.2,134.1,250.3,156.0,251.5,220.1,62.1,37.3]:: halts3(c1,f5(c1),f5(c1)),outputs(c1,good),halts2(c2,f6(c2)) -> program(c3)
% 1.42/0.83 === Conflict found: 228:6:1:[27.5,140.1]:Top: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),halts2(f5(x0),f5(x0)) -> halts2(f6(c2),f6(c2)),outputs(c2,bad) {x0 -> c1}
% 1.42/0.83 === Backtracking. Learning clause 254:4:0:[129.1,253.2,228.1,62.1]:: halts3(c1,f5(c1),f5(c1)),outputs(c1,good) -> halts2(f6(c2),f6(c2)),outputs(c2,bad)
% 1.42/0.83 === Backtracking. Learning clause 256:3:0:[129.1,255.0,46.1,141.1,219.1,25.7,230.7,62.1,254.4,248.4,252.4]:: halts3(c1,f5(c1),f5(c1)),outputs(c1,good),halts2(c2,f6(c2)) ->
% 1.42/0.83 === Conflict found: 55:6:2:[26.5,24.5]:TopTop: program(x0),halts3(x0,f5(x0),f5(x0)),outputs(x0,good),halts2(f5(x0),f5(x0)),program(x1) -> halts2(c2,x1) {x0 -> c1, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 257:2:0:[55.5,140.1,129.2,62.1,256.3]:: halts3(c1,f5(c1),f5(c1)),outputs(c1,good) ->
% 1.42/0.83 === Backtracking. Learning clause 258:4:1:[17.2,140.1]:Top: program(x0) -> program(f5(x0)),halts2(f6(c2),f6(c2)),outputs(c2,bad)
% 1.42/0.83 === Conflict found: 80:2:2:[49.0,79.0,50.1,2.3,4.2]:TopTop: program(x0) -> decides(c1,x0,x1) {x0 -> f4(c1), x1 -> f3(c1)}
% 1.42/0.83 === Backtracking. Learning clause 261:5:2:[62.0,259.0,257.1,260.4,80.2,10.2,246.2,258.2,156.1]:TopTop: halts2(f5(x0),x1),halts3(c1,f5(c1),f5(c1)),program(x0) -> outputs(c2,bad),program(c3)
% 1.42/0.83 === Conflict found: 227:4:1:[156.1,226.1,42.6,219.1,141.1,225.4]:Top: halts2(c2,f6(c2)),program(x0),halts2(f6(c2),f6(c2)) -> program(f5(x0)) {x0 -> c1}
% 1.42/0.83 === Backtracking. Learning clause 262:4:1:[227.3,258.3]:Top: halts2(c2,f6(c2)),program(x0) -> program(f5(x0)),outputs(c2,bad)
% 1.42/0.83 === Conflict found: 161:6:2:[62.0,160.0,6.4,80.1,91.2,129.2]:TopTop: program(f5(c1)),program(x0),halts2(x0,x0),halts3(c1,f5(c1),f5(c1)) -> decides(c1,f4(c1),x1),outputs(c2,good) {x0 -> c3, x1 -> f3(c1)}
% 1.42/0.83 === Backtracking. Learning clause 265:4:0:[62.0,263.0,248.1,264.5,161.5,10.2,42.3,141.1,219.1,129.2,156.2]:: program(f5(c1)),halts2(c2,f6(c2)),halts3(c1,f5(c1),f5(c1)),halts2(f6(c2),f6(c2)) ->
% 1.42/0.83 === Conflict found: 261:5:2:[62.0,259.0,257.1,260.4,80.2,10.2,246.2,258.2,156.1]:TopTop: halts2(f5(x0),x1),halts3(c1,f5(c1),f5(c1)),program(x0) -> outputs(c2,bad),program(c3) {x0 -> c1, x1 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 267:3:0:[62.0,266.0,261.1,129.2]:: halts3(c1,f5(c1),f5(c1)) -> outputs(c2,bad),program(c3)
% 1.42/0.83 === Conflict found: 53:4:2:[16.3,14.2]:TopTop: program(x0),program(x1) -> program(f5(x0)),halts2(c2,x1) {x0 -> c1, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 268:3:1:[53.2,140.1,262.1]:Top: program(x0) -> program(f5(x0)),outputs(c2,bad)
% 1.42/0.83 === Conflict found: 161:6:2:[62.0,160.0,6.4,80.1,91.2,129.2]:TopTop: program(f5(c1)),program(x0),halts2(x0,x0),halts3(c1,f5(c1),f5(c1)) -> decides(c1,f4(c1),x1),outputs(c2,good) {x0 -> c3, x1 -> f3(c1)}
% 1.42/0.83 === Backtracking. Learning clause 271:5:1:[62.0,269.4,91.1,270.6,161.5,10.2]:Top: program(f5(c1)),program(x0),halts2(x0,x0),halts3(c1,f5(c1),f5(c1)) -> outputs(c2,good)
% 1.42/0.83 === Conflict found: 153:6:4:[62.0,152.3,55.3,6.5,129.2,51.4,80.1]:TopTopTopTop: program(x0),program(x1),halts2(x1,x2),program(f5(c1)) -> halts2(c2,x0),decides(c1,f4(c1),x3) {x0 -> f6(c2), x1 -> f5(c1), x2 -> f5(c1), x3 -> f3(c1)}
% 1.42/0.83 === Backtracking. Learning clause 274:3:0:[62.0,272.0,257.1,273.4,153.6,10.2,140.1,129.2,265.2]:: program(f5(c1)),halts3(c1,f5(c1),f5(c1)),halts2(f6(c2),f6(c2)) ->
% 1.42/0.83 === Conflict found: 80:2:2:[49.0,79.0,50.1,2.3,4.2]:TopTop: program(x0) -> decides(c1,x0,x1) {x0 -> f4(c1), x1 -> f3(c1)}
% 1.42/0.83 === Backtracking. Learning clause 277:2:0:[62.0,275.1,257.1,276.2,80.1,246.2,10.2,129.2,268.2]:: halts3(c1,f5(c1),f5(c1)) -> outputs(c2,bad)
% 1.42/0.83 === Conflict found: 227:4:1:[156.1,226.1,42.6,219.1,141.1,225.4]:Top: halts2(c2,f6(c2)),program(x0),halts2(f6(c2),f6(c2)) -> program(f5(x0)) {x0 -> c1}
% 1.42/0.83 === Backtracking. Learning clause 278:3:0:[227.2,62.1]:: halts2(c2,f6(c2)),halts2(f6(c2),f6(c2)) -> program(f5(c1))
% 1.42/0.83 === Conflict found: 53:4:2:[16.3,14.2]:TopTop: program(x0),program(x1) -> program(f5(x0)),halts2(c2,x1) {x0 -> c1, x1 -> f6(c2)}
% 1.42/0.83 === Backtracking. Learning clause 279:2:0:[53.1,62.1,140.1,278.1]:: halts2(f6(c2),f6(c2)) -> program(f5(c1))
% 1.42/0.83 === Conflict found: 80:2:2:[49.0,79.0,50.1,2.3,4.2]:TopTop: program(x0) -> decides(c1,x0,x1) {x0 -> f4(c1), x1 -> f3(c1)}
% 1.42/0.83 === Backtracking. Learning clause 280:2:1:[80.1,246.2]:Top: halts3(c1,f5(c1),f5(c1)) -> decides(c1,f4(c1),x0)
% 1.42/0.83 === Conflict found: 278:3:0:[227.2,62.1]:: halts2(c2,f6(c2)),halts2(f6(c2),f6(c2)) -> program(f5(c1)) {}
% 1.42/0.83 === Backtracking. Learning clause 281:3:0:[278.3,265.1]:: halts2(c2,f6(c2)),halts3(c1,f5(c1),f5(c1)),halts2(f6(c2),f6(c2)) ->
% 1.42/0.83 === Backtracking. Learning clause 283:3:0:[156.0,282.2,37.1,141.1]:: halts2(c2,f6(c2)),outputs(c2,bad) -> program(c3)
% 1.42/0.83 === Backtracking. Learning clause 284:2:1:[10.5,257.2,141.1,62.1,280.2]:Top: halts2(c2,x0),halts3(c1,f5(c1),f5(c1)) ->
% 1.42/0.83 === Conflict found: 274:3:0:[62.0,272.0,257.1,273.4,153.6,10.2,140.1,129.2,265.2]:: program(f5(c1)),halts3(c1,f5(c1),f5(c1)),halts2(f6(c2),f6(c2)) -> {}
% 1.42/0.83 === Backtracking. Learning clause 285:2:0:[274.1,279.2]:: halts3(c1,f5(c1),f5(c1)),halts2(f6(c2),f6(c2)) ->
% 1.42/0.83 === Backtracking. Learning clause 287:2:0:[279.0,286.1,16.2,140.1,62.1]:: -> program(f5(c1)),halts2(c2,f6(c2))
% 1.42/0.83 === Backtracking. Learning clause 288:1:0:[10.5,257.2,129.2,280.2,62.1,287.1,284.1]:: halts3(c1,f5(c1),f5(c1)) ->
% 1.42/0.83 === Backtracking. Learning clause 291:4:1:[13.2,289.0,156.0,290.5,37.3,258.4]:Top: halts2(c2,f6(c2)),program(x0) -> program(c3),program(f5(x0))
% 1.42/0.83 === Backtracking. Learning clause 292:1:0:[38.5,219.1,141.1,258.4,291.3,62.1,279.1,287.2]:: -> program(f5(c1))
% 1.42/0.83 === Conflict found: 51:4:3:[7.3,5.2]:TopTopTop: program(x0),program(x1) -> program(f4(x0)),halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83 === Backtracking. Learning clause 295:1:1:[62.0,293.0,292.0,294.1,51.4,288.1,80.1]:Top: -> decides(c1,f4(c1),x0)
% 1.42/0.83 === Backtracking. Learning clause 299:1:0:[62.0,296.0,164.2,297.1,292.0,298.2,11.5,288.1]:: -> halts2(f5(c1),f5(c1))
% 1.42/0.83 === Conflict found: 52:4:3:[11.3,9.3]:TopTopTop: program(x0),decides(x0,f4(x0),f3(x0)),program(x1) -> halts3(x0,x1,x2) {x0 -> c1, x1 -> f5(c1), x2 -> f5(c1)}
% 1.42/0.83
% 1.42/0.83 SZS status Unsatisfiable
% 1.42/0.83
% 1.42/0.83 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.83
% 1.42/0.83 SPASS-SCL-FOL Statistics:
% 1.42/0.83 Number of learned clauses: 124
% 1.42/0.83 Number of propagations: 737
% 1.42/0.83 Number of decisions: 463
% 1.42/0.83 Number of resolutions: 353
% 1.42/0.83 Number of condensations: 35
% 1.42/0.83 Number of sub resolutions: 125
% 1.42/0.83 Number of input literals (deduplicated): 28
% 1.42/0.83 Number of grows: 5
% 1.42/0.83 Number of considered ground atoms: 115
% 1.42/0.83
% 1.42/0.83 Needed: 0:00:00.27
% 1.42/0.83
%------------------------------------------------------------------------------