%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN542+1 : TPTP v9.2.1. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:59 PM UTC 2026
% Result : CounterSatisfiable 58.97s 15.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SYN542+1 : TPTP v9.2.1. Released v2.1.0.
% 0.11/0.14 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.35 % Computer : n020.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Thu May 7 13:45:51 EDT 2026
% 0.15/0.35 % CPUTime :
% 0.15/0.35 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 58.97/15.21 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.97/15.21 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.97/15.21 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.97/15.21 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.97/15.21 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.97/15.21 Execution resolution_3 ended with status: satisfiable
% 58.97/15.21 Used heuristic: resolution_3
% 58.97/15.21
% 58.97/15.21 Input Clauses:
% 58.97/15.21
% 58.97/15.21 Predicates: hskp0 ndr1_0 c2_1 c4_1 c0_1 hskp1 c3_1 c5_1 hskp2 c1_1 hskp3 hskp4 hskp5 hskp6 hskp7 hskp8 hskp9 hskp10 hskp11 hskp12 hskp13 hskp14 hskp15 hskp16 hskp17 hskp18 hskp19 hskp20 hskp21 hskp22 hskp23 hskp24 hskp25 hskp26 hskp27 hskp28 hskp29 hskp30 hskp31 hskp32 hskp33 hskp34 hskp35 hskp36 hskp37 hskp38 hskp39 hskp40 hskp41 hskp42 hskp43 hskp44 hskp45 hskp46 hskp47 hskp48 hskp49 hskp50 hskp51 hskp52 hskp53 hskp54 hskp55 hskp56 hskp57 hskp58 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 ren38 ren39 ren40 ren41 ren42 ren43 ren44 ren45 ren46 ren47 ren48 ren49 ren50 ren51 ren52 ren53 ren54 ren55 ren56 ren57 ren58 ren59
% 58.97/15.21 Fol Constants: a1 a3 a5 a6 a7 a8 a9 a10 a11 a12 a14 a15 a17 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 a32 a33 a34 a35 a36 a37 a41 a45 a46 a49 a50 a51 a54 a59 a61 a62 a66 a67 a68 a71 a73 a75 a76 a2 a4 a40 a42 a44 a47 a56 a60 a63 a64
% 58.97/15.21 Fol Functions:
% 58.97/15.21 Problem Properties:
% 58.97/15.21 This is a Bernays Schoenfinkel problem.
% 58.97/15.21
% 58.97/15.21 After reduction: Problem Properties:
% 58.97/15.21 This is a Bernays Schoenfinkel problem.
% 58.97/15.21
% 58.97/15.21
% 58.97/15.21 Reduced Input Clauses:
% 58.97/15.21
% 58.97/15.21 Most General Atoms: ren1 ndr1_0 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 ren38 ren39 ren40 ren41 ren42 ren43 ren44 ren45 ren46 ren47 ren48 ren49 ren50 ren51 ren52 ren53 ren54 ren55 ren56 ren57 ren58 ren59 hskp0 hskp1 hskp2 hskp3 hskp4 hskp5 hskp6 hskp7 hskp8 hskp9 hskp10 hskp11 hskp12 hskp13 hskp14 hskp15 hskp16 hskp17 hskp18 hskp19 hskp20 hskp21 hskp22 hskp23 hskp24 hskp25 hskp26 hskp27 hskp28 hskp29 hskp30 hskp31 hskp32 hskp33 hskp34 hskp35 hskp36 hskp37 hskp38 hskp39 hskp40 hskp41 hskp42 hskp43 hskp44 hskp45 hskp46 hskp47 hskp48 hskp49 hskp50 hskp51 hskp52 hskp53 hskp54 hskp55 hskp56 hskp57 hskp58 c0_1(x0) c2_1(x1) c3_1(x2) c4_1(x2) c5_1(x2) c1_1(x1)
% 58.97/15.21
% 58.97/15.21 === Starting SPASS-SCL-FOL A Little Less Naive, considering 51 atoms initially, heuristics mode: resolution_3 ===
% 58.97/15.21
% 58.97/15.21 === Backtracking. Learning clause 350:2:0:[1.1,237.2]:: hskp0 -> ndr1_0
% 58.97/15.21 === Clause set with instances from active satisfied. Growing active. New size: 115
% 58.97/15.21 === Restarting.
% 58.97/15.21 === Clause set with instances from active satisfied. Growing active. New size: 184
% 58.97/15.21 === Restarting.
% 58.97/15.21 === Clause set with instances from active satisfied. Growing active. New size: 260
% 58.97/15.21 === Restarting.
% 58.97/15.21 === Backtracking. Learning clause 353:8:1:[45.1,351.2,170.1,352.3,296.8,48.2,171.2]:Top: c2_1(x0),c4_1(x0),c4_1(a66),ren12,ren43 -> c0_1(a15),c2_1(a15),c3_1(x0)
% 58.97/15.21 === Conflict found: 353:8:1:[45.1,351.2,170.1,352.3,296.8,48.2,171.2]:Top: c2_1(x0),c4_1(x0),c4_1(a66),ren12,ren43 -> c0_1(a15),c2_1(a15),c3_1(x0) {x0 -> a12}
% 58.97/15.21 === Backtracking. Learning clause 355:7:0:[38.1,354.0,353.8,40.2]:: c4_1(a12),c4_1(a66),ren12,ren43,ren10 -> c0_1(a15),c2_1(a15)
% 58.97/15.21 === Backtracking. Learning clause 360:6:1:[49.1,356.2,170.1,357.3,50.1,358.7,52.1,359.8,296.8,51.2,171.2]:Top: c2_1(x0),c4_1(x0),c4_1(a66),ren13,ren43 -> c3_1(x0)
% 58.97/15.21 === Conflict found: 360:6:1:[49.1,356.2,170.1,357.3,50.1,358.7,52.1,359.8,296.8,51.2,171.2]:Top: c2_1(x0),c4_1(x0),c4_1(a66),ren13,ren43 -> c3_1(x0) {x0 -> a12}
% 58.97/15.21 === Backtracking. Learning clause 362:5:0:[38.1,361.0,360.6,40.2]:: c4_1(a12),c4_1(a66),ren13,ren43,ren10 ->
% 58.97/15.21 === Backtracking. Learning clause 366:7:1:[69.1,363.0,71.1,364.1,80.1,365.8,299.6,79.2,72.2]:Top: ren20,ren18 -> c0_1(x0),c2_1(x0),c4_1(x0),c3_1(a25),c5_1(a23)
% 58.97/15.21 === Backtracking. Learning clause 370:7:1:[45.1,367.0,46.1,368.1,80.1,369.8,299.6,79.2,48.2]:Top: ren20,ren12 -> c0_1(x0),c2_1(x0),c4_1(x0),c3_1(a25),c5_1(a15)
% 58.97/15.21 === Backtracking. Learning clause 374:7:1:[77.1,371.0,154.1,372.1,80.1,373.8,299.9,156.2,79.2]:Top: ren39,ren20 -> c0_1(x0),c2_1(x0),c4_1(x0),c3_1(a25),c5_1(a54)
% 58.97/15.21 === Clause set with instances from active satisfied. Growing active. New size: 348
% 58.97/15.21 === Restarting.
% 58.97/15.21 === Backtracking. Learning clause 377:8:2:[25.1,375.3,28.1,376.9,306.6,26.2]:TopTop: c2_1(x0),c2_1(x1),c4_1(x1),c0_1(a9),ren7 -> c0_1(x0),c5_1(x0),c0_1(x1)
% 58.97/15.21 === Backtracking. Learning clause 379:9:2:[45.1,378.2,296.8,48.2]:TopTop: c2_1(x0),c4_1(x0),c0_1(x1),c4_1(x1),c5_1(x1),ren12 -> c0_1(a15),c2_1(a15),c3_1(x0)
% 58.97/15.21 === Backtracking. Learning clause 383:5:0:[25.1,380.1,27.1,381.6,28.1,382.7,320.7,51.2,26.2]:: c4_1(a17),c5_1(a9),ren13,ren7 -> c5_1(a17)
% 58.97/15.21 === Backtracking. Learning clause 387:4:0:[25.1,384.1,27.1,385.5,28.1,386.6,320.7,91.2,26.2,92.2]:: c4_1(a28),c5_1(a9),ren7,ren23 ->
% 58.97/15.21 === Backtracking. Learning clause 389:9:2:[25.1,388.1,327.2,26.2]:TopTop: c0_1(x0),c0_1(x1),c5_1(x1),ren7 -> c2_1(x0),c4_1(x0),c4_1(a9),c5_1(a9),c4_1(x1)
% 58.97/15.21 === Conflict found: 389:9:2:[25.1,388.1,327.2,26.2]:TopTop: c0_1(x0),c0_1(x1),c5_1(x1),ren7 -> c2_1(x0),c4_1(x0),c4_1(a9),c5_1(a9),c4_1(x1) {x0 -> a66, x1 -> a62}
% 58.97/15.21 === Backtracking. Learning clause 391:9:0:[168.1,390.9,389.3,167.2,387.2,170.2]:: c0_1(a62),ren42,c4_1(a28),ren7,ren23,ren43 -> c2_1(a66),c4_1(a66),c4_1(a9)
% 58.97/15.21 === Conflict found: 389:9:2:[25.1,388.1,327.2,26.2]:TopTop: c0_1(x0),c0_1(x1),c5_1(x1),ren7 -> c2_1(x0),c4_1(x0),c4_1(a9),c5_1(a9),c4_1(x1) {x0 -> a66, x1 -> a66}
% 58.97/15.21 === Backtracking. Learning clause 392:9:0:[389.3,171.2,387.2,170.2,362.2]:: c4_1(a28),ren7,ren23,c4_1(a12),ren13,ren43,ren10 -> c2_1(a66),c4_1(a9)
% 58.97/15.21 === Backtracking. Learning clause 396:7:0:[9.1,393.0,90.1,394.1,11.1,395.7,300.9,91.2,10.2,132.2]:: ren23,ren3,ren33 -> c0_1(a41),c2_1(a41),c4_1(a5),c4_1(a28)
% 58.97/15.21 === Backtracking. Learning clause 400:7:1:[9.1,397.0,90.1,398.1,11.1,399.7,300.9,91.2,10.2]:Top: ren23,ren3 -> c0_1(x0),c2_1(x0),c5_1(x0),c4_1(a5),c4_1(a28)
% 58.97/15.21 === Backtracking. Learning clause 403:7:2:[93.1,401.1,95.1,402.7,327.2,94.2,96.2]:TopTop: c0_1(x0),c0_1(x1),c5_1(x1),ren24 -> c2_1(x0),c4_1(x0),c4_1(x1)
% 58.97/15.21 === Conflict found: 403:7:2:[93.1,401.1,95.1,402.7,327.2,94.2,96.2]:TopTop: c0_1(x0),c0_1(x1),c5_1(x1),ren24 -> c2_1(x0),c4_1(x0),c4_1(x1) {x0 -> a66, x1 -> a62}
% 58.97/15.21 === Backtracking. Learning clause 405:6:0:[168.1,404.6,403.3,167.2,170.2]:: c0_1(a62),ren24,ren42,ren43 -> c2_1(a66),c4_1(a66)
% 58.97/15.21 === Conflict found: 403:7:2:[93.1,401.1,95.1,402.7,327.2,94.2,96.2]:TopTop: c0_1(x0),c0_1(x1),c5_1(x1),ren24 -> c2_1(x0),c4_1(x0),c4_1(x1) {x0 -> a66, x1 -> a66}
% 58.97/15.21 === Backtracking. Learning clause 406:6:0:[403.3,171.2,170.2,362.2]:: ren24,c4_1(a12),ren13,ren43,ren10 -> c2_1(a66)
% 58.97/15.21 === Conflict found: 403:7:2:[93.1,401.1,95.1,402.7,327.2,94.2,96.2]:TopTop: c0_1(x0),c0_1(x1),c5_1(x1),ren24 -> c2_1(x0),c4_1(x0),c4_1(x1) {x0 -> a62, x1 -> a62}
% 58.97/15.21 === Backtracking. Learning clause 408:6:1:[168.1,407.6,403.3,167.2]:Top: c0_1(x0),c0_1(a62),ren24,ren42 -> c2_1(x0),c4_1(x0)
% 58.97/15.21 === Conflict found: 403:7:2:[93.1,401.1,95.1,402.7,327.2,94.2,96.2]:TopTop: c0_1(x0),c0_1(x1),c5_1(x1),ren24 -> c2_1(x0),c4_1(x0),c4_1(x1) {x0 -> a9, x1 -> a42}
% 58.97/15.21 === Backtracking. Learning clause 409:7:1:[403.3,212.2]:Top: c0_1(x0),c0_1(a42),ren24,ren53 -> c2_1(x0),c4_1(x0),c4_1(a42)
% 58.97/15.21 === Backtracking. Learning clause 412:9:1:[93.1,410.1,108.1,411.7,307.1,106.2,403.3,403.3,236.2]:Top: c2_1(a32),ren27,c0_1(a64),c0_1(x0),ren24,ren59 -> c4_1(a64),c2_1(x0),c4_1(x0)
% 58.97/15.21 === Backtracking. Learning clause 415:8:1:[93.1,413.1,108.1,414.7,307.1,106.2,152.2,403.3,151.2]:Top: c2_1(a32),c0_1(a51),ren27,c0_1(x0),ren24,ren38 -> c2_1(x0),c4_1(x0)
% 58.97/15.21 === Conflict found: 377:8:2:[25.1,375.3,28.1,376.9,306.6,26.2]:TopTop: c2_1(x0),c2_1(x1),c4_1(x1),c0_1(a9),ren7 -> c0_1(x0),c5_1(x0),c0_1(x1) {x0 -> a51, x1 -> a23}
% 58.97/15.21 === Backtracking. Learning clause 416:13:2:[377.7,152.2,415.2]:TopTop: c2_1(a51),c2_1(x0),c4_1(x0),c0_1(a9),ren7,c2_1(a32),ren27,c0_1(x1),ren24,ren38 -> c0_1(x0),c2_1(x1),c4_1(x1)
% 58.97/15.21 === Backtracking. Learning clause 420:6:0:[93.1,417.2,108.1,418.7,95.1,419.8,307.1,106.2,152.2,96.2,151.2]:: c2_1(a32),c0_1(a29),c0_1(a51),ren27,ren24,ren38 ->
% 58.97/15.21 === Backtracking. Learning clause 423:8:1:[37.1,421.0,40.1,422.7,299.9,188.2,39.2]:Top: c3_1(a73),ren47,ren10 -> c0_1(x0),c2_1(x0),c4_1(x0),c4_1(a12),c5_1(a73)
% 58.97/15.21 === Clause set with instances from active satisfied. Growing active. New size: 412
% 58.97/15.21 === Restarting.
% 58.97/15.21 === Backtracking. Learning clause 428:9:1:[21.1,424.2,24.1,425.8,95.1,426.9,36.1,427.12,307.1,22.2,96.2,403.3,35.2]:Top: c2_1(a8),c0_1(a29),ren6,c0_1(x0),c0_1(a11),ren24,ren9 -> c2_1(x0),c4_1(x0)
% 58.97/15.21 === Backtracking. Learning clause 434:11:0:[21.1,429.1,24.1,430.9,135.1,431.10,59.1,432.13,36.1,433.15,307.1,22.2,403.3,403.3,35.2,226.2,134.2,58.2]:: c2_1(a8),ren6,c0_1(a11),ren24,ren9,ren57,ren34,ren15 -> c4_1(a45),c4_1(a60),c4_1(a20)
% 58.97/15.21 === Backtracking. Learning clause 437:7:0:[13.1,435.1,59.1,436.7,307.1,22.2,403.3,16.2,15.2,102.2,58.2,24.2,14.2,104.2]:: c2_1(a8),ren24,ren15,ren6,ren4,ren26 -> c4_1(a20)
% 58.97/15.21 === Conflict found: 428:9:1:[21.1,424.2,24.1,425.8,95.1,426.9,36.1,427.12,307.1,22.2,96.2,403.3,35.2]:Top: c2_1(a8),c0_1(a29),ren6,c0_1(x0),c0_1(a11),ren24,ren9 -> c2_1(x0),c4_1(x0) {x0 -> a45}
% 58.97/15.21 === Backtracking. Learning clause 439:8:0:[135.1,438.7,428.4,134.2]:: c2_1(a8),c0_1(a29),ren6,c0_1(a11),ren24,ren9,ren34 -> c4_1(a45)
% 58.97/15.21 === Backtracking. Learning clause 444:9:0:[21.1,440.1,24.1,441.8,135.1,442.10,36.1,443.12,307.1,22.2,403.3,403.3,35.2,226.2,134.2]:: c2_1(a8),ren6,c0_1(a11),ren24,ren9,ren57,ren34 -> c4_1(a60),c4_1(a45)
% 58.97/15.21 === Backtracking. Learning clause 448:7:0:[13.1,445.1,135.1,446.7,104.1,447.9,307.1,22.2,403.3,16.2,15.2,134.2,102.2,24.2,14.2]:: c2_1(a8),ren24,ren34,ren26,ren6,ren4 -> c4_1(a45)
% 58.97/15.21 === Conflict found: 428:9:1:[21.1,424.2,24.1,425.8,95.1,426.9,36.1,427.12,307.1,22.2,96.2,403.3,35.2]:Top: c2_1(a8),c0_1(a29),ren6,c0_1(x0),c0_1(a11),ren24,ren9 -> c2_1(x0),c4_1(x0) {x0 -> a61}
% 58.97/15.21 === Backtracking. Learning clause 450:8:0:[163.1,449.8,428.4,162.2]:: c2_1(a8),c0_1(a29),ren6,c0_1(a11),ren24,ren9,ren41 -> c2_1(a61)
% 58.97/15.21 === Conflict found: 415:8:1:[93.1,413.1,108.1,414.7,307.1,106.2,152.2,403.3,151.2]:Top: c2_1(a32),c0_1(a51),ren27,c0_1(x0),ren24,ren38 -> c2_1(x0),c4_1(x0) {x0 -> a61}
% 58.97/15.21 === Backtracking. Learning clause 452:7:0:[163.1,451.7,415.4,162.2]:: c2_1(a32),c0_1(a51),ren27,ren24,ren38,ren41 -> c2_1(a61)
% 58.97/15.21 === Backtracking. Learning clause 457:9:0:[21.1,453.1,24.1,454.8,163.1,455.11,36.1,456.12,307.1,22.2,403.3,403.3,35.2,226.2,162.2]:: c2_1(a8),ren6,c0_1(a11),ren24,ren9,ren57,ren41 -> c4_1(a60),c2_1(a61)
% 58.97/15.21 === Backtracking. Learning clause 459:7:0:[13.1,458.1,307.1,22.2,403.3,16.2,15.2,162.2,102.2,24.2,14.2,163.2,104.2]:: c2_1(a8),ren24,ren6,ren4,ren41,ren26 -> c2_1(a61)
% 58.97/15.21 === Backtracking. Learning clause 461:4:0:[13.1,460.1,307.1,22.2,164.2,16.2,15.2,162.2,24.2,14.2,163.2]:: c2_1(a8),ren6,ren4,ren41 ->
% 58.97/15.21 === Backtracking. Learning clause 464:8:0:[9.1,462.2,12.1,463.8,320.7,51.2,22.2,10.2]:: c4_1(a17),c5_1(a5),c5_1(a8),ren13,ren6,ren3 -> c5_1(a17),c3_1(a8)
% 58.97/15.21 === Backtracking. Learning clause 467:7:0:[9.1,465.2,12.1,466.7,320.7,91.2,22.2,10.2,92.2]:: c4_1(a28),c5_1(a5),c5_1(a8),ren6,ren3,ren23 -> c3_1(a8)
% 58.97/15.21 === Backtracking. Learning clause 470:6:0:[9.1,468.1,12.1,469.6,320.7,51.2,10.2]:: c4_1(a17),c5_1(a5),ren13,ren3 -> c5_1(a17),c3_1(a5)
% 58.97/15.21 === Backtracking. Learning clause 473:5:0:[9.1,471.1,12.1,472.5,320.7,91.2,10.2,92.2]:: c4_1(a28),c5_1(a5),ren3,ren23 -> c3_1(a5)
% 58.97/15.21 === Backtracking. Learning clause 475:7:0:[21.1,474.1,320.7,51.2,22.2]:: c4_1(a17),c5_1(a8),ren13,ren6 -> c5_1(a17),c2_1(a8),c3_1(a8)
% 58.97/15.21 === Backtracking. Learning clause 477:6:0:[21.1,476.1,320.7,91.2,22.2,92.2]:: c4_1(a28),c5_1(a8),ren6,ren23 -> c2_1(a8),c3_1(a8)
% 58.97/15.21 === Backtracking. Learning clause 479:9:1:[93.1,478.3,306.6,94.2,180.2]:Top: c2_1(a68),c2_1(x0),c4_1(x0),c0_1(a29),ren24,ren45 -> c0_1(a68),c0_1(x0),c3_1(a29)
% 58.97/15.21 === Backtracking. Learning clause 482:8:1:[101.1,480.3,102.1,481.4,306.6,103.2,180.2]:Top: c2_1(a68),c2_1(x0),c4_1(x0),ren26,ren45 -> c0_1(a68),c0_1(x0),c3_1(a31)
% 58.97/15.21 === Backtracking. Learning clause 489:14:2:[162.1,483.1,93.1,484.2,102.1,485.6,108.1,486.13,163.1,487.14,104.1,488.17,307.1,106.2,164.2,403.3,482.8]:TopTop: c2_1(a32),ren27,ren41,c0_1(x0),ren24,c2_1(a68),c2_1(x1),c4_1(x1),ren26,ren45 -> c2_1(x0),c4_1(x0),c0_1(a68),c0_1(x1)
% 58.97/15.21 === Backtracking. Learning clause 492:8:1:[5.1,490.3,6.1,491.7,306.6,94.2,8.2]:Top: c2_1(a3),c2_1(x0),c4_1(x0),c0_1(a29),ren24,ren2 -> c0_1(x0),c3_1(a29)
% 58.97/15.21 === Backtracking. Learning clause 496:7:1:[5.1,493.3,102.1,494.4,6.1,495.7,306.6,103.2,8.2]:Top: c2_1(a3),c2_1(x0),c4_1(x0),ren26,ren2 -> c0_1(x0),c3_1(a31)
% 58.97/15.21 === Backtracking. Learning clause 501:12:0:[1.1,497.0,2.1,498.7,3.1,499.8,59.1,500.14,307.1,106.2,180.2,403.3,496.7,489.13,108.2,102.2,58.2,4.2,179.2,104.2]:: c2_1(a3),ren2,c2_1(a32),ren41,ren24,c2_1(a68),ren27,ren15,ren1,ren45,ren26 -> c4_1(a20)
% 58.97/15.21 === Backtracking. Learning clause 508:14:0:[1.1,502.0,2.1,503.2,3.1,504.3,75.1,505.10,104.1,506.17,135.1,507.18,307.1,106.2,180.2,403.3,496.7,489.13,134.2,108.2,102.2,76.2,4.2,179.2]:: c2_1(a3),ren2,c2_1(a32),ren41,ren24,c2_1(a68),c2_1(a24),ren34,ren27,ren26,ren19,ren1,ren45 -> c4_1(a45)
% 58.97/15.21 === Backtracking. Learning clause 511:13:0:[1.1,509.0,2.1,510.2,307.1,106.2,180.2,403.3,496.7,489.13,162.2,108.2,102.2,76.2,4.2,179.2,163.2,104.2,75.2,3.2]:: c2_1(a3),ren2,c2_1(a32),ren24,c2_1(a68),c2_1(a24),ren27,ren45,ren41,ren26,ren19,ren1 -> c2_1(a61)
% 58.97/15.21 === Backtracking. Learning clause 516:10:0:[1.1,512.1,2.1,513.4,3.1,514.5,59.1,515.12,307.1,106.2,164.2,403.3,496.7,162.2,108.2,102.2,58.2,4.2,163.2,104.2]:: c2_1(a32),ren24,c2_1(a3),ren2,ren27,ren15,ren1,ren41,ren26 -> c4_1(a20)
% 58.97/15.21 === Backtracking. Learning clause 522:10:0:[1.1,517.1,2.1,518.4,3.1,519.5,135.1,520.12,104.1,521.14,307.1,106.2,164.2,403.3,496.7,162.2,134.2,108.2,102.2,4.2,163.2]:: c2_1(a32),ren24,c2_1(a3),ren2,ren34,ren27,ren26,ren1,ren41 -> c4_1(a45)
% 58.97/15.21 === Backtracking. Learning clause 525:9:0:[1.1,523.1,2.1,524.4,307.1,106.2,164.2,403.3,496.7,162.2,108.2,102.2,4.2,163.2,104.2,3.2]:: c2_1(a32),ren24,c2_1(a3),ren2,ren27,ren41,ren26,ren1 -> c2_1(a61)
% 58.97/15.21 === Backtracking. Learning clause 528:10:1:[5.1,526.1,163.1,527.10,307.1,106.2,164.2,96.2,492.8,162.2,108.2]:Top: c2_1(a32),c2_1(a3),c2_1(x0),c4_1(x0),c0_1(a29),ren24,ren2,ren41,ren27 -> c0_1(x0)
% 58.97/15.21 === Backtracking. Learning clause 531:7:0:[13.1,529.2,14.1,530.3,307.1,94.2,152.2,16.2,15.2]:: c2_1(a29),c0_1(a51),ren24,ren38,ren4 -> c0_1(a29),c4_1(a51)
% 58.97/15.21 === Backtracking. Learning clause 534:9:0:[1.1,532.1,2.1,533.4,307.1,94.2,164.2,16.2,15.2,162.2,528.5,14.2,4.2,163.2,3.2]:: c2_1(a29),c2_1(a32),c2_1(a3),ren24,ren2,ren27,ren4,ren41,ren1 ->
% 58.97/15.21 === Conflict found: 377:8:2:[25.1,375.3,28.1,376.9,306.6,26.2]:TopTop: c2_1(x0),c2_1(x1),c4_1(x1),c0_1(a9),ren7 -> c0_1(x0),c5_1(x0),c0_1(x1) {x0 -> a3, x1 -> a1}
% 58.97/15.21 === Backtracking. Learning clause 536:7:1:[6.1,535.6,377.7,8.2]:Top: c2_1(a3),c2_1(x0),c4_1(x0),c0_1(a9),ren7,ren2 -> c0_1(x0)
% 58.97/15.21 === Backtracking. Learning clause 540:8:1:[111.1,537.0,93.1,538.1,112.1,539.7,307.1,110.2,403.3,403.3,236.2]:Top: ren28,c0_1(a64),c0_1(x0),ren24,ren59 -> c4_1(a64),c2_1(x0),c4_1(x0)
% 58.97/15.21 === Backtracking. Learning clause 542:9:0:[49.1,541.2,320.5,110.2,106.2,51.2]:: c4_1(a17),c5_1(a32),c5_1(a33),ren28,ren27,ren13 -> c5_1(a17),c2_1(a32),c3_1(a33)
% 58.97/15.21 === Backtracking. Learning clause 546:7:1:[111.1,543.0,93.1,544.1,112.1,545.7,307.1,110.2,152.2,403.3,151.2]:Top: c0_1(a51),ren28,c0_1(x0),ren24,ren38 -> c2_1(x0),c4_1(x0)
% 58.97/15.21 === Backtracking. Learning clause 554:12:0:[111.1,547.0,1.1,548.1,2.1,549.4,3.1,550.5,163.1,551.14,59.1,552.16,104.1,553.18,307.1,110.2,403.3,403.3,496.7,226.2,162.2,112.2,102.2,58.2,4.2]:: ren24,c2_1(a3),ren2,ren57,ren41,ren28,ren26,ren15,ren1 -> c2_1(a61),c4_1(a60),c4_1(a20)
% 58.97/15.21 === Backtracking. Learning clause 560:9:0:[111.1,555.0,1.1,556.1,2.1,557.4,3.1,558.5,59.1,559.12,307.1,110.2,164.2,403.3,496.7,162.2,112.2,102.2,58.2,4.2,163.2,104.2]:: ren24,c2_1(a3),ren2,ren28,ren15,ren1,ren41,ren26 -> c4_1(a20)
% 58.97/15.21 === Backtracking. Learning clause 568:12:0:[111.1,561.0,1.1,562.1,2.1,563.4,3.1,564.5,163.1,565.14,135.1,566.16,104.1,567.18,307.1,110.2,403.3,403.3,496.7,226.2,162.2,134.2,112.2,102.2,4.2]:: ren24,c2_1(a3),ren2,ren57,ren41,ren34,ren28,ren26,ren1 -> c2_1(a61),c4_1(a60),c4_1(a45)
% 58.97/15.21 === Backtracking. Learning clause 575:9:0:[111.1,569.0,1.1,570.1,2.1,571.4,3.1,572.5,135.1,573.12,104.1,574.14,307.1,110.2,164.2,403.3,496.7,162.2,134.2,112.2,102.2,4.2,163.2]:: ren24,c2_1(a3),ren2,ren34,ren28,ren26,ren1,ren41 -> c4_1(a45)
% 58.97/15.21 === Conflict found: 546:7:1:[111.1,543.0,93.1,544.1,112.1,545.7,307.1,110.2,152.2,403.3,151.2]:Top: c0_1(a51),ren28,c0_1(x0),ren24,ren38 -> c2_1(x0),c4_1(x0) {x0 -> a61}
% 58.97/15.21 === Backtracking. Learning clause 577:6:0:[163.1,576.6,546.3,162.2]:: c0_1(a51),ren28,ren24,ren38,ren41 -> c2_1(a61)
% 58.97/15.21 === Backtracking. Learning clause 584:10:0:[111.1,578.0,1.1,579.1,2.1,580.4,3.1,581.5,163.1,582.14,104.1,583.15,307.1,110.2,403.3,403.3,496.7,226.2,162.2,112.2,102.2,4.2]:: ren24,c2_1(a3),ren2,ren57,ren41,ren28,ren26,ren1 -> c4_1(a60),c2_1(a61)
% 58.97/15.21 === Backtracking. Learning clause 588:8:0:[111.1,585.0,1.1,586.1,2.1,587.4,307.1,110.2,164.2,403.3,496.7,162.2,112.2,102.2,4.2,163.2,104.2,3.2]:: ren24,c2_1(a3),ren2,ren28,ren41,ren26,ren1 -> c2_1(a61)
% 58.97/15.21 === Backtracking. Learning clause 593:5:0:[111.1,589.0,93.1,590.2,112.1,591.7,95.1,592.8,307.1,110.2,152.2,96.2,151.2]:: c0_1(a29),c0_1(a51),ren28,ren24,ren38 ->
% 58.97/15.21 === Backtracking. Learning clause 597:9:1:[111.1,594.0,5.1,595.1,163.1,596.10,307.1,110.2,164.2,96.2,492.8,162.2,112.2]:Top: c2_1(a3),c2_1(x0),c4_1(x0),c0_1(a29),ren24,ren2,ren41,ren28 -> c0_1(x0)
% 58.97/15.21 === Backtracking. Learning clause 600:8:0:[1.1,598.1,2.1,599.3,307.1,94.2,164.2,16.2,15.2,162.2,597.4,14.2,4.2,163.2,3.2]:: c2_1(a29),c2_1(a3),ren24,ren2,ren28,ren4,ren41,ren1 ->
% 58.97/15.21 === Backtracking. Learning clause 604:5:0:[105.1,601.1,108.1,602.6,163.1,603.7,307.1,106.2,164.2,152.2,151.2,162.2]:: c2_1(a32),c0_1(a51),ren27,ren38,ren41 ->
% 58.97/15.21 === Backtracking. Learning clause 606:4:0:[13.1,605.1,307.1,106.2,164.2,16.2,15.2,162.2,108.2,14.2,163.2]:: c2_1(a32),ren27,ren4,ren41 ->
% 58.97/15.21 === Backtracking. Learning clause 611:4:0:[111.1,607.0,109.1,608.1,112.1,609.6,163.1,610.7,307.1,110.2,164.2,152.2,151.2,162.2]:: c0_1(a51),ren28,ren38,ren41 ->
% 58.97/15.21 === Backtracking. Learning clause 612:4:0:[307.1,110.2,164.2,16.2,15.2,162.2,112.2,14.2,163.2,111.2,277.2,264.2,240.2]:: ndr1_0,hskp40,hskp27,hskp3 ->
% 58.97/15.21 === Backtracking. Learning clause 614:3:0:[13.1,613.0,307.1,110.2,164.2,16.2,15.2,162.2,112.2,14.2,163.2,111.2]:: ren4,ren41,ren28 ->
% 58.97/15.21 === Backtracking. Learning clause 618:9:1:[5.1,615.1,24.1,616.9,95.1,617.10,307.1,22.2,96.2,492.8]:Top: c2_1(a8),ren6,c2_1(a3),c2_1(x0),c4_1(x0),c0_1(a29),ren24,ren2 -> c0_1(x0)
% 58.97/15.21 === Backtracking. Learning clause 620:5:0:[129.1,619.1,320.2,166.2,130.2,167.2,132.2]:: c4_1(a41),ren42,ren33 -> c2_1(a62),c3_1(a62)
% 58.97/15.21 === Backtracking. Learning clause 622:7:0:[109.1,621.1,320.2,166.2,130.2,110.2,167.2,132.2]:: c4_1(a41),c5_1(a33),ren28,ren42,ren33 -> c2_1(a62),c3_1(a33)
% 58.97/15.21 === Backtracking. Learning clause 624:9:1:[93.1,623.3,306.6,210.2,96.2]:Top: c2_1(a29),c2_1(x0),c4_1(x0),c0_1(a42),ren53,ren24 -> c0_1(a29),c0_1(x0),c3_1(a42)
% 58.97/15.21 === Backtracking. Learning clause 627:8:1:[93.1,625.3,226.1,626.4,306.6,227.2,96.2]:Top: c2_1(a29),c2_1(x0),c4_1(x0),ren57,ren24 -> c0_1(a29),c0_1(x0),c3_1(a60)
% 58.97/15.21 === Clause set with instances from active satisfied. Growing active. New size: 429
% 58.97/15.21 === Restarting.
% 58.97/15.21 === Clause set with instances from active satisfied. Growing active. New size: 442
% 58.97/15.21 === Clause set with instances from active satisfied. Growing active. New size: 473
% 58.97/15.21
% 58.97/15.21 Linear Model Building succeeded.
% 58.97/15.21 SZS status Satisfiable
% 58.97/15.21
% 58.97/15.21 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.97/15.21
% 58.97/15.21 SPASS-SCL-FOL Statistics:
% 58.97/15.21 Number of learned clauses: 82
% 58.97/15.21 Number of propagations: 9164
% 58.97/15.21 Number of decisions: 5264
% 58.97/15.21 Number of resolutions: 386
% 58.97/15.21 Number of condensations: 4
% 58.97/15.21 Number of sub resolutions: 196
% 58.97/15.21 Number of input literals (deduplicated): 302
% 58.97/15.21 Number of grows: 8
% 58.97/15.21 Number of considered ground atoms: 473
% 58.97/15.21
% 58.97/15.21 Needed: 0:0:14.64
% 58.97/15.21
%------------------------------------------------------------------------------