%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN313-1.001.002 : 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 : n004.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 0.29s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN313-1.001.002 : 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.17/0.33 % Computer : n004.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % 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 13:40:18 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.29/0.55 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.29/0.55 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.29/0.55 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.29/0.55 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.29/0.55 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.29/0.55 Execution resolution_3 ended with status: unsatisfiable
% 0.29/0.55 Used heuristic: resolution_3
% 0.29/0.55
% 0.29/0.55 Input Clauses:
% 0.29/0.55
% 0.29/0.55 Predicates: p
% 0.29/0.55 Fol Constants: h0
% 0.29/0.55 Fol Functions: f0 f1 j0 h1 j1 h2 j2
% 0.29/0.55 Problem Properties:
% 0.29/0.55 This is a full first-order problem without equality.
% 0.29/0.55
% 0.29/0.55 After reduction: Problem Properties:
% 0.29/0.55 This is a full first-order problem without equality.
% 0.29/0.55
% 0.29/0.55
% 0.29/0.55 Reduced Input Clauses:
% 0.29/0.55
% 0.29/0.55 Most General Atoms: p(x0,f0(x0),x1) p(x0,f1(x1),x2) p(h0,x0,j0(x1)) p(h1(x0),x2,j1(x1)) p(h2(x2),x1,j2(x1))
% 0.29/0.55
% 0.29/0.55 === Starting SPASS-SCL-FOL A Little Less Naive, considering 8 atoms initially, heuristics mode: resolution_3 ===
% 0.29/0.55
% 0.29/0.55 === Backtracking. Learning clause 3:3:3:[1.2,2.3]:TopTopTop: p(h2(x0),f0(h2(x0)),x1) -> p(h0,x2,j0(f1(x1))),p(h1(x2),x0,j1(f1(x1)))
% 0.29/0.55 === Backtracking. Learning clause 4:3:3:[1.1,2.3]:TopTopTop: p(h2(x0),f1(j2(f0(h2(x0)))),x1) -> p(h0,x2,j0(f0(h2(x0)))),p(h1(x2),x0,j1(f0(h2(x0))))
% 0.29/0.55 === Clause set with instances from active satisfied. Growing active. New size: 11
% 0.29/0.55 === Restarting.
% 0.29/0.55 === Conflict found: 3:3:3:[1.2,2.3]:TopTopTop: p(h2(x0),f0(h2(x0)),x1) -> p(h0,x2,j0(f1(x1))),p(h1(x2),x0,j1(f1(x1))) {x0 -> h0, x1 -> j2(f0(h2(h0))), x2 -> h0}
% 0.29/0.55 === Backtracking. Learning clause 5:4:3:[3.1,2.3]:TopTopTop: -> p(h0,x0,j0(f1(j2(f0(h2(x1)))))),p(h1(x0),x1,j1(f1(j2(f0(h2(x1)))))),p(h0,x2,j0(f0(h2(x1)))),p(h1(x2),x1,j1(f0(h2(x1))))
% 0.29/0.55 === Clause set with instances from active satisfied. Growing active. New size: 21
% 0.29/0.55 === Restarting.
% 0.29/0.55 === Conflict found: 5:4:3:[3.1,2.3]:TopTopTop: -> p(h0,x0,j0(f1(j2(f0(h2(x1)))))),p(h1(x0),x1,j1(f1(j2(f0(h2(x1)))))),p(h0,x2,j0(f0(h2(x1)))),p(h1(x2),x1,j1(f0(h2(x1)))) {x0 -> h0, x1 -> f1(h0), x2 -> h0}
% 0.29/0.55 === Backtracking. Learning clause 6:4:3:[5.2,1.2,1.2]:TopTopTop: p(h1(x0),f0(h1(x0)),x1),p(h1(x2),f0(h1(x2)),x1) -> p(h0,x0,j0(f1(j2(f0(h2(f1(x1))))))),p(h0,x2,j0(f0(h2(f1(x1)))))
% 0.29/0.55 === Backtracking. Learning clause 7:4:3:[1.1,5.2]:TopTopTop: p(h1(x0),f1(j1(f1(j2(f0(h2(f0(h1(x0)))))))),x1) -> p(h0,x0,j0(f1(j2(f0(h2(f0(h1(x0)))))))),p(h0,x2,j0(f0(h2(f0(h1(x0)))))),p(h1(x2),f0(h1(x0)),j1(f0(h2(f0(h1(x0))))))
% 0.29/0.55 === Clause set with instances from active satisfied. Growing active. New size: 28
% 0.29/0.55 === Restarting.
% 0.29/0.55 === Conflict found: 6:4:3:[5.2,1.2,1.2]:TopTopTop: p(h1(x0),f0(h1(x0)),x1),p(h1(x2),f0(h1(x2)),x1) -> p(h0,x0,j0(f1(j2(f0(h2(f1(x1))))))),p(h0,x2,j0(f0(h2(f1(x1))))) {x0 -> f1(h0), x1 -> h0, x2 -> h0}
% 0.29/0.55 === Backtracking. Learning clause 8:4:3:[6.3,1.2]:TopTopTop: p(h1(f1(x0)),f0(h1(f1(x0))),x1),p(h1(x2),f0(h1(x2)),x1),p(h0,f0(h0),x0) -> p(h0,x2,j0(f0(h2(f1(x1)))))
% 0.29/0.55 === Clause set with instances from active satisfied. Growing active. New size: 39
% 0.29/0.55 === Restarting.
% 0.29/0.55 === Backtracking. Learning clause 9:5:3:[2.2,8.1]:TopTopTop: p(h1(x0),f0(h1(x0)),j1(x1)),p(h0,f0(h0),x2) -> p(h0,f1(x2),j0(x1)),p(h2(f0(h1(f1(x2)))),x1,j2(x1)),p(h0,x0,j0(f0(h2(f1(j1(x1))))))
% 0.29/0.55 === Conflict found: 8:4:3:[6.3,1.2]:TopTopTop: p(h1(f1(x0)),f0(h1(f1(x0))),x1),p(h1(x2),f0(h1(x2)),x1),p(h0,f0(h0),x0) -> p(h0,x2,j0(f0(h2(f1(x1))))) {x0 -> h0, x1 -> j1(f1(j2(f0(h2(f0(h1(f1(h0)))))))), x2 -> h0}
% 0.29/0.55 === Backtracking. Learning clause 10:6:3:[8.1,5.2]:TopTopTop: p(h1(x0),f0(h1(x0)),j1(f1(j2(f0(h2(f0(h1(f1(x1))))))))),p(h0,f0(h0),x1) -> p(h0,x0,j0(f0(h2(f1(j1(f1(j2(f0(h2(f0(h1(f1(x1))))))))))))),p(h0,f1(x1),j0(f1(j2(f0(h2(f0(h1(f1(x1))))))))),p(h0,x2,j0(f0(h2(f0(h1(f1(x1))))))),p(h1(x2),f0(h1(f1(x1))),j1(f0(h2(f0(h1(f1(x1)))))))
% 0.29/0.55 === Clause set with instances from active satisfied. Growing active. New size: 48
% 0.29/0.55 === Restarting.
% 0.29/0.55 === Conflict found: 10:6:3:[8.1,5.2]:TopTopTop: p(h1(x0),f0(h1(x0)),j1(f1(j2(f0(h2(f0(h1(f1(x1))))))))),p(h0,f0(h0),x1) -> p(h0,x0,j0(f0(h2(f1(j1(f1(j2(f0(h2(f0(h1(f1(x1))))))))))))),p(h0,f1(x1),j0(f1(j2(f0(h2(f0(h1(f1(x1))))))))),p(h0,x2,j0(f0(h2(f0(h1(f1(x1))))))),p(h1(x2),f0(h1(f1(x1))),j1(f0(h2(f0(h1(f1(x1))))))) {x0 -> f1(h0), x1 -> h0, x2 -> h0}
% 0.29/0.55 === Backtracking. Learning clause 11:4:2:[10.1,5.2,1.2]:TopTop: p(h0,f0(h0),x0) -> p(h0,f1(x0),j0(f1(j2(f0(h2(f0(h1(f1(x0))))))))),p(h0,x1,j0(f0(h2(f0(h1(f1(x0))))))),p(h1(x1),f0(h1(f1(x0))),j1(f0(h2(f0(h1(f1(x0)))))))
% 0.29/0.55 === Conflict found: 3:3:3:[1.2,2.3]:TopTopTop: p(h2(x0),f0(h2(x0)),x1) -> p(h0,x2,j0(f1(x1))),p(h1(x2),x0,j1(f1(x1))) {x0 -> f0(h1(f1(h0))), x1 -> j2(f0(h2(f0(h1(f1(h0)))))), x2 -> f1(h0)}
% 0.29/0.55 === Backtracking. Learning clause 12:7:3:[3.1,9.4,8.1]:TopTopTop: p(h1(x0),f0(h1(x0)),j1(f0(h2(f0(h1(f1(x1))))))),p(h1(x2),f0(h1(x2)),j1(f1(j2(f0(h2(f0(h1(f1(x1))))))))),p(h0,f0(h0),x1) -> p(h0,f1(x1),j0(f1(j2(f0(h2(f0(h1(f1(x1))))))))),p(h0,f1(x1),j0(f0(h2(f0(h1(f1(x1))))))),p(h0,x0,j0(f0(h2(f1(j1(f0(h2(f0(h1(f1(x1))))))))))),p(h0,x2,j0(f0(h2(f1(j1(f1(j2(f0(h2(f0(h1(f1(x1)))))))))))))
% 0.29/0.55 === Conflict found: 3:3:3:[1.2,2.3]:TopTopTop: p(h2(x0),f0(h2(x0)),x1) -> p(h0,x2,j0(f1(x1))),p(h1(x2),x0,j1(f1(x1))) {x0 -> f0(h1(f1(h0))), x1 -> j2(f0(h2(f0(h1(f1(h0)))))), x2 -> f1(h0)}
% 0.29/0.55 === Backtracking. Learning clause 13:5:2:[3.1,9.4,12.2,1.2]:TopTop: p(h1(x0),f0(h1(x0)),j1(f0(h2(f0(h1(f1(x1))))))),p(h0,f0(h0),x1) -> p(h0,f1(x1),j0(f1(j2(f0(h2(f0(h1(f1(x1))))))))),p(h0,f1(x1),j0(f0(h2(f0(h1(f1(x1))))))),p(h0,x0,j0(f0(h2(f1(j1(f0(h2(f0(h1(f1(x1)))))))))))
% 0.29/0.55 === Clause set with instances from active satisfied. Growing active. New size: 51
% 0.29/0.55 === Restarting.
% 0.29/0.55 === Conflict found: 8:4:3:[6.3,1.2]:TopTopTop: p(h1(f1(x0)),f0(h1(f1(x0))),x1),p(h1(x2),f0(h1(x2)),x1),p(h0,f0(h0),x0) -> p(h0,x2,j0(f0(h2(f1(x1))))) {x0 -> h0, x1 -> j1(f0(h2(f0(h1(f1(h0)))))), x2 -> f1(h0)}
% 0.29/0.55 === Backtracking. Learning clause 14:1:1:[8.1,11.4,1.2,1.2,1.2]:Top: p(h0,f0(h0),x0) ->
% 0.29/0.55 === Clause set with instances from active satisfied. Growing active. New size: 53
% 0.29/0.55 === Restarting.
% 0.29/0.55 === Conflict found: 6:4:3:[5.2,1.2,1.2]:TopTopTop: p(h1(x0),f0(h1(x0)),x1),p(h1(x2),f0(h1(x2)),x1) -> p(h0,x0,j0(f1(j2(f0(h2(f1(x1))))))),p(h0,x2,j0(f0(h2(f1(x1))))) {x0 -> f0(h0), x1 -> h0, x2 -> h0}
% 0.29/0.55 === Backtracking. Learning clause 15:3:2:[6.3,14.1]:TopTop: p(h1(f0(h0)),f0(h1(f0(h0))),x0),p(h1(x1),f0(h1(x1)),x0) -> p(h0,x1,j0(f0(h2(f1(x0)))))
% 0.29/0.55 === Clause set with instances from active satisfied. Growing active. New size: 63
% 0.29/0.55 === Restarting.
% 0.29/0.55 === Backtracking. Learning clause 16:4:2:[2.2,15.1]:TopTop: p(h1(x0),f0(h1(x0)),j1(x1)) -> p(h0,f0(h0),j0(x1)),p(h2(f0(h1(f0(h0)))),x1,j2(x1)),p(h0,x0,j0(f0(h2(f1(j1(x1))))))
% 0.29/0.55 === Conflict found: 15:3:2:[6.3,14.1]:TopTop: p(h1(f0(h0)),f0(h1(f0(h0))),x0),p(h1(x1),f0(h1(x1)),x0) -> p(h0,x1,j0(f0(h2(f1(x0))))) {x0 -> j1(f1(j2(f0(h2(f0(h1(f0(h0)))))))), x1 -> h0}
% 0.29/0.55 === Backtracking. Learning clause 17:5:2:[15.1,5.2]:TopTop: p(h1(x0),f0(h1(x0)),j1(f1(j2(f0(h2(f0(h1(f0(h0))))))))) -> p(h0,x0,j0(f0(h2(f1(j1(f1(j2(f0(h2(f0(h1(f0(h0))))))))))))),p(h0,f0(h0),j0(f1(j2(f0(h2(f0(h1(f0(h0))))))))),p(h0,x1,j0(f0(h2(f0(h1(f0(h0))))))),p(h1(x1),f0(h1(f0(h0))),j1(f0(h2(f0(h1(f0(h0)))))))
% 0.29/0.55 === Clause set with instances from active satisfied. Growing active. New size: 72
% 0.29/0.55 === Restarting.
% 0.29/0.55 === Conflict found: 17:5:2:[15.1,5.2]:TopTop: p(h1(x0),f0(h1(x0)),j1(f1(j2(f0(h2(f0(h1(f0(h0))))))))) -> p(h0,x0,j0(f0(h2(f1(j1(f1(j2(f0(h2(f0(h1(f0(h0))))))))))))),p(h0,f0(h0),j0(f1(j2(f0(h2(f0(h1(f0(h0))))))))),p(h0,x1,j0(f0(h2(f0(h1(f0(h0))))))),p(h1(x1),f0(h1(f0(h0))),j1(f0(h2(f0(h1(f0(h0))))))) {x0 -> f0(h0), x1 -> h0}
% 0.29/0.55 === Backtracking. Learning clause 18:3:1:[17.1,5.2,14.1]:Top: -> p(h0,f0(h0),j0(f1(j2(f0(h2(f0(h1(f0(h0))))))))),p(h0,x0,j0(f0(h2(f0(h1(f0(h0))))))),p(h1(x0),f0(h1(f0(h0))),j1(f0(h2(f0(h1(f0(h0)))))))
% 0.29/0.55 === Conflict found: 3:3:3:[1.2,2.3]:TopTopTop: p(h2(x0),f0(h2(x0)),x1) -> p(h0,x2,j0(f1(x1))),p(h1(x2),x0,j1(f1(x1))) {x0 -> f0(h1(f0(h0))), x1 -> j2(f0(h2(f0(h1(f0(h0)))))), x2 -> f0(h0)}
% 0.29/0.55 === Backtracking. Learning clause 19:6:2:[3.1,16.3,15.1]:TopTop: p(h1(x0),f0(h1(x0)),j1(f0(h2(f0(h1(f0(h0))))))),p(h1(x1),f0(h1(x1)),j1(f1(j2(f0(h2(f0(h1(f0(h0))))))))) -> p(h0,f0(h0),j0(f1(j2(f0(h2(f0(h1(f0(h0))))))))),p(h0,f0(h0),j0(f0(h2(f0(h1(f0(h0))))))),p(h0,x0,j0(f0(h2(f1(j1(f0(h2(f0(h1(f0(h0))))))))))),p(h0,x1,j0(f0(h2(f1(j1(f1(j2(f0(h2(f0(h1(f0(h0)))))))))))))
% 0.29/0.55 === Conflict found: 3:3:3:[1.2,2.3]:TopTopTop: p(h2(x0),f0(h2(x0)),x1) -> p(h0,x2,j0(f1(x1))),p(h1(x2),x0,j1(f1(x1))) {x0 -> f0(h1(f0(h0))), x1 -> j2(f0(h2(f0(h1(f0(h0)))))), x2 -> f0(h0)}
% 0.29/0.55 === Backtracking. Learning clause 20:4:1:[3.1,16.3,19.2,14.1]:Top: p(h1(x0),f0(h1(x0)),j1(f0(h2(f0(h1(f0(h0))))))) -> p(h0,f0(h0),j0(f1(j2(f0(h2(f0(h1(f0(h0))))))))),p(h0,f0(h0),j0(f0(h2(f0(h1(f0(h0))))))),p(h0,x0,j0(f0(h2(f1(j1(f0(h2(f0(h1(f0(h0)))))))))))
% 0.29/0.55 === Clause set with instances from active satisfied. Growing active. New size: 75
% 0.29/0.55 === Restarting.
% 0.29/0.55 === Conflict found: 15:3:2:[6.3,14.1]:TopTop: p(h1(f0(h0)),f0(h1(f0(h0))),x0),p(h1(x1),f0(h1(x1)),x0) -> p(h0,x1,j0(f0(h2(f1(x0))))) {x0 -> j1(f0(h2(f0(h1(f0(h0)))))), x1 -> f0(h0)}
% 0.29/0.55
% 0.29/0.55 SZS status Unsatisfiable
% 0.29/0.55
% 0.29/0.55 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.29/0.55
% 0.29/0.55 SPASS-SCL-FOL Statistics:
% 0.29/0.55 Number of learned clauses: 18
% 0.29/0.55 Number of propagations: 357
% 0.29/0.55 Number of decisions: 326
% 0.29/0.55 Number of resolutions: 34
% 0.29/0.55 Number of condensations: 4
% 0.29/0.55 Number of sub resolutions: 0
% 0.29/0.55 Number of input literals (deduplicated): 5
% 0.29/0.55 Number of grows: 10
% 0.29/0.55 Number of considered ground atoms: 75
% 0.29/0.55
% 0.29/0.55 Needed: 0:00:00.04
% 0.29/0.55
%------------------------------------------------------------------------------