%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SET863-2 : TPTP v9.2.1. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n023.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:33:32 PM UTC 2026
% Result : Unsatisfiable 0.90s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET863-2 : TPTP v9.2.1. Released v3.2.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.33 % Computer : n023.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Thu May 7 13:09:39 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.90/0.66 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.90/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.90/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.90/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.90/0.66 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.90/0.66 Execution resolution_2 ended with status: unsatisfiable
% 0.90/0.66 Used heuristic: resolution_2
% 0.90/0.66
% 0.90/0.66 Input Clauses:
% 0.90/0.66
% 0.90/0.66 Predicates: c_in c_lessequals
% 0.90/0.66 Fol Constants: c_emptyset v_c v_S t_a v_x v_y v_xa
% 0.90/0.66 Fol Functions: tc_set c_Main_OsubsetI__1 c_Zorn_Ochain c_Zorn_Ochain__extend__1 c_insert c_union c_Zorn_Omaxchain c_Zorn_Omaxchain__super__lemma__1
% 0.90/0.66 Problem Properties:
% 0.90/0.66 This is a full first-order problem without equality.
% 0.90/0.66
% 0.90/0.66 After reduction: Problem Properties:
% 0.90/0.66 This is a full first-order problem without equality.
% 0.90/0.66
% 0.90/0.66
% 0.90/0.66 Reduced Input Clauses:
% 0.90/0.66
% 0.90/0.66 Most General Atoms: c_lessequals(x0,x1,tc_set(x2)) c_in(x0,x5,x2)
% 0.90/0.66
% 0.90/0.66 === Starting SPASS-SCL-FOL A Little Less Naive, considering 48 atoms initially, heuristics mode: resolution_2 ===
% 0.90/0.66
% 0.90/0.66 === Clause set with instances from active satisfied. Growing active. New size: 58
% 0.90/0.66 === Restarting.
% 0.90/0.66 === Backtracking. Learning clause 15:4:3:[6.1,8.1]:TopTopTop: c_in(x0,c_Zorn_Omaxchain(x1,tc_set(tc_set(t_a))),tc_set(tc_set(tc_set(tc_set(t_a))))),c_in(c_union(c_insert(c_Zorn_Omaxchain(v_S,t_a),c_emptyset,tc_set(tc_set(tc_set(t_a)))),x0,tc_set(tc_set(tc_set(t_a)))),c_Zorn_Ochain(x1,tc_set(tc_set(t_a))),tc_set(tc_set(tc_set(tc_set(t_a))))) -> c_in(v_c,x2,tc_set(tc_set(t_a))),c_in(c_Zorn_Omaxchain__super__lemma__1(x0,x2,tc_set(tc_set(t_a))),x0,tc_set(tc_set(tc_set(t_a))))
% 0.90/0.66 === Backtracking. Learning clause 16:3:1:[5.1,8.1]:Top: c_in(x0,c_Zorn_Ochain(c_Zorn_Omaxchain(v_S,t_a),tc_set(t_a)),tc_set(tc_set(tc_set(t_a)))),c_lessequals(c_Zorn_Ochain__extend__1(x0,v_c,tc_set(t_a)),v_c,tc_set(tc_set(t_a))) -> c_in(c_union(c_insert(v_c,c_emptyset,tc_set(tc_set(t_a))),x0,tc_set(tc_set(t_a))),c_Zorn_Ochain(c_Zorn_Omaxchain(v_S,t_a),tc_set(t_a)),tc_set(tc_set(tc_set(t_a))))
% 0.90/0.66 === Backtracking. Learning clause 17:3:1:[4.1,8.1]:Top: c_in(x0,c_Zorn_Ochain(c_Zorn_Omaxchain(v_S,t_a),tc_set(t_a)),tc_set(tc_set(tc_set(t_a)))) -> c_in(c_Zorn_Ochain__extend__1(x0,v_c,tc_set(t_a)),x0,tc_set(tc_set(t_a))),c_in(c_union(c_insert(v_c,c_emptyset,tc_set(tc_set(t_a))),x0,tc_set(tc_set(t_a))),c_Zorn_Ochain(c_Zorn_Omaxchain(v_S,t_a),tc_set(t_a)),tc_set(tc_set(tc_set(t_a))))
% 0.90/0.66 === Backtracking. Learning clause 18:2:1:[1.1,8.1]:Top: c_lessequals(c_Zorn_Omaxchain(v_S,t_a),x0,tc_set(tc_set(tc_set(t_a)))) -> c_in(v_c,x0,tc_set(tc_set(t_a)))
% 0.90/0.66 === Clause set with instances from active satisfied. Growing active. New size: 64
% 0.90/0.66 === Restarting.
% 0.90/0.66 === Backtracking. Learning clause 19:4:3:[6.1,9.1]:TopTopTop: c_in(x0,c_Zorn_Omaxchain(x1,tc_set(tc_set(t_a))),tc_set(tc_set(tc_set(tc_set(t_a))))),c_in(c_union(c_insert(c_Zorn_Ochain(v_S,t_a),c_emptyset,tc_set(tc_set(tc_set(t_a)))),x0,tc_set(tc_set(tc_set(t_a)))),c_Zorn_Ochain(x1,tc_set(tc_set(t_a))),tc_set(tc_set(tc_set(tc_set(t_a))))) -> c_in(v_c,x2,tc_set(tc_set(t_a))),c_in(c_Zorn_Omaxchain__super__lemma__1(x0,x2,tc_set(tc_set(t_a))),x0,tc_set(tc_set(tc_set(t_a))))
% 0.90/0.66 === Backtracking. Learning clause 20:4:3:[7.1,9.1]:TopTopTop: c_in(x0,c_Zorn_Omaxchain(x1,tc_set(tc_set(t_a))),tc_set(tc_set(tc_set(tc_set(t_a))))),c_in(c_union(c_insert(c_Zorn_Ochain(v_S,t_a),c_emptyset,tc_set(tc_set(tc_set(t_a)))),x0,tc_set(tc_set(tc_set(t_a)))),c_Zorn_Ochain(x1,tc_set(tc_set(t_a))),tc_set(tc_set(tc_set(tc_set(t_a))))),c_lessequals(c_Zorn_Omaxchain__super__lemma__1(x0,x2,tc_set(tc_set(t_a))),x2,tc_set(tc_set(tc_set(t_a)))) -> c_in(v_c,x2,tc_set(tc_set(t_a)))
% 0.90/0.66 === Backtracking. Learning clause 21:3:1:[5.2,9.1]:Top: c_in(x0,v_S,tc_set(t_a)),c_lessequals(c_Zorn_Ochain__extend__1(v_c,x0,t_a),x0,tc_set(t_a)) -> c_in(c_union(c_insert(x0,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
% 0.90/0.66 === Backtracking. Learning clause 22:3:1:[4.2,9.1]:Top: c_in(x0,v_S,tc_set(t_a)) -> c_in(c_Zorn_Ochain__extend__1(v_c,x0,t_a),v_c,tc_set(t_a)),c_in(c_union(c_insert(x0,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
% 0.90/0.66 === Backtracking. Learning clause 23:1:2:[3.1,2.1]:TopTop: -> c_lessequals(x0,x0,tc_set(x1))
% 0.90/0.66 === Clause set with instances from active satisfied. Growing active. New size: 77
% 0.90/0.66 === Restarting.
% 0.90/0.66 === Backtracking. Learning clause 24:4:3:[6.1,10.1]:TopTopTop: c_in(x0,c_Zorn_Omaxchain(x1,tc_set(t_a)),tc_set(tc_set(tc_set(t_a)))),c_in(c_union(c_insert(v_S,c_emptyset,tc_set(tc_set(t_a))),x0,tc_set(tc_set(t_a))),c_Zorn_Ochain(x1,tc_set(t_a)),tc_set(tc_set(tc_set(t_a)))) -> c_in(v_x,x2,tc_set(t_a)),c_in(c_Zorn_Omaxchain__super__lemma__1(x0,x2,tc_set(t_a)),x0,tc_set(tc_set(t_a)))
% 0.90/0.66 === Backtracking. Learning clause 25:3:1:[5.1,10.1]:Top: c_in(x0,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a))),c_lessequals(c_Zorn_Ochain__extend__1(x0,v_x,t_a),v_x,tc_set(t_a)) -> c_in(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),x0,tc_set(t_a)),c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
% 0.90/0.66 === Conflict found: 25:3:1:[5.1,10.1]:Top: c_in(x0,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a))),c_lessequals(c_Zorn_Ochain__extend__1(x0,v_x,t_a),v_x,tc_set(t_a)) -> c_in(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),x0,tc_set(t_a)),c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a))) {x0 -> v_c}
% 0.90/0.66 === Backtracking. Learning clause 26:2:0:[25.1,9.1]:: c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x,t_a),v_x,tc_set(t_a)) -> c_in(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
% 0.90/0.66 === Clause set with instances from active satisfied. Growing active. New size: 79
% 0.90/0.66 === Restarting.
% 0.90/0.66 === Backtracking. Learning clause 27:2:1:[1.2,11.1]:Top: c_in(x0,v_y,t_a) -> c_in(x0,v_x,t_a)
% 0.90/0.66 === Clause set with instances from active satisfied. Growing active. New size: 143
% 0.90/0.66 === Backtracking. Learning clause 28:4:3:[14.2,7.4,6.5]:TopTopTop: c_in(x0,x1,t_a),c_in(v_c,c_Zorn_Omaxchain(x2,t_a),tc_set(tc_set(t_a))),c_in(c_union(c_insert(x1,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),c_Zorn_Ochain(x2,t_a),tc_set(tc_set(t_a))) -> c_in(x0,v_y,t_a)
% 0.90/0.66 === Clause set with instances from active satisfied. Growing active. New size: 150
% 0.90/0.66 === Restarting.
% 0.90/0.66 === Backtracking. Learning clause 29:4:3:[6.1,12.1]:TopTopTop: c_in(x0,c_Zorn_Omaxchain(x1,t_a),tc_set(tc_set(t_a))),c_in(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),x0,tc_set(t_a)),c_Zorn_Ochain(x1,t_a),tc_set(tc_set(t_a))) -> c_in(v_xa,x2,t_a),c_in(c_Zorn_Omaxchain__super__lemma__1(x0,x2,t_a),x0,tc_set(t_a))
% 0.90/0.66 === Conflict found: 28:4:3:[14.2,7.4,6.5]:TopTopTop: c_in(x0,x1,t_a),c_in(v_c,c_Zorn_Omaxchain(x2,t_a),tc_set(tc_set(t_a))),c_in(c_union(c_insert(x1,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),c_Zorn_Ochain(x2,t_a),tc_set(tc_set(t_a))) -> c_in(x0,v_y,t_a) {x0 -> v_xa, x1 -> v_x, x2 -> c_emptyset}
% 0.90/0.66 === Backtracking. Learning clause 30:2:1:[28.1,12.1,13.1]:Top: c_in(v_c,c_Zorn_Omaxchain(x0,t_a),tc_set(tc_set(t_a))),c_in(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),c_Zorn_Ochain(x0,t_a),tc_set(tc_set(t_a))) ->
% 0.90/0.66 === Clause set with instances from active satisfied. Growing active. New size: 152
% 0.90/0.66 === Restarting.
% 0.90/0.66 === Backtracking. Learning clause 31:2:1:[1.1,12.1]:Top: c_lessequals(v_x,x0,tc_set(t_a)) -> c_in(v_xa,x0,t_a)
% 0.90/0.66 === Clause set with instances from active satisfied. Growing active. New size: 158
% 0.90/0.66 === Restarting.
% 0.90/0.66 === Backtracking. Learning clause 32:4:1:[5.2,26.2]:Top: c_in(x0,v_S,tc_set(t_a)),c_lessequals(c_Zorn_Ochain__extend__1(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),x0,t_a),x0,tc_set(t_a)),c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x,t_a),v_x,tc_set(t_a)) -> c_in(c_union(c_insert(x0,c_emptyset,tc_set(t_a)),c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),tc_set(t_a)),c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
% 0.90/0.66 === Conflict found: 25:3:1:[5.1,10.1]:Top: c_in(x0,c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a))),c_lessequals(c_Zorn_Ochain__extend__1(x0,v_x,t_a),v_x,tc_set(t_a)) -> c_in(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),x0,tc_set(t_a)),c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a))) {x0 -> c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a))}
% 0.90/0.66 === Backtracking. Learning clause 33:3:0:[25.1,26.2]:: c_lessequals(c_Zorn_Ochain__extend__1(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),v_x,t_a),v_x,tc_set(t_a)),c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x,t_a),v_x,tc_set(t_a)) -> c_in(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),tc_set(t_a)),c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a)))
% 0.90/0.66 === Conflict found: 29:4:3:[6.1,12.1]:TopTopTop: c_in(x0,c_Zorn_Omaxchain(x1,t_a),tc_set(tc_set(t_a))),c_in(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),x0,tc_set(t_a)),c_Zorn_Ochain(x1,t_a),tc_set(tc_set(t_a))) -> c_in(v_xa,x2,t_a),c_in(c_Zorn_Omaxchain__super__lemma__1(x0,x2,t_a),x0,tc_set(t_a)) {x0 -> v_c, x1 -> v_S, x2 -> c_emptyset}
% 0.90/0.66 === Backtracking. Learning clause 35:3:1:[8.0,34.0,29.2,26.2]:Top: c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x,t_a),v_x,tc_set(t_a)) -> c_in(v_xa,x0,t_a),c_in(c_Zorn_Omaxchain__super__lemma__1(v_c,x0,t_a),v_c,tc_set(t_a))
% 0.90/0.66 === Conflict found: 30:2:1:[28.1,12.1,13.1]:Top: c_in(v_c,c_Zorn_Omaxchain(x0,t_a),tc_set(tc_set(t_a))),c_in(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),c_Zorn_Ochain(x0,t_a),tc_set(tc_set(t_a))) -> {x0 -> v_S}
% 0.90/0.66 === Backtracking. Learning clause 36:1:0:[30.2,26.2,8.1]:: c_lessequals(c_Zorn_Ochain__extend__1(v_c,v_x,t_a),v_x,tc_set(t_a)) ->
% 0.90/0.66 === Clause set with instances from active satisfied. Growing active. New size: 160
% 0.90/0.66 === Restarting.
% 0.90/0.66 === Backtracking. Learning clause 37:1:0:[2.2,36.1]:: -> c_in(c_Main_OsubsetI__1(c_Zorn_Ochain__extend__1(v_c,v_x,t_a),v_x,t_a),c_Zorn_Ochain__extend__1(v_c,v_x,t_a),t_a)
% 0.90/0.66 === Conflict found: 30:2:1:[28.1,12.1,13.1]:Top: c_in(v_c,c_Zorn_Omaxchain(x0,t_a),tc_set(tc_set(t_a))),c_in(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),c_Zorn_Ochain(x0,t_a),tc_set(tc_set(t_a))) -> {x0 -> v_S}
% 0.90/0.66 === Backtracking. Learning clause 38:1:0:[30.1,8.1]:: c_in(c_union(c_insert(v_x,c_emptyset,tc_set(t_a)),v_c,tc_set(t_a)),c_Zorn_Ochain(v_S,t_a),tc_set(tc_set(t_a))) ->
% 0.90/0.66 === Clause set with instances from active satisfied. Growing active. New size: 224
% 0.90/0.66
% 0.90/0.66 SZS status Unsatisfiable
% 0.90/0.66
% 0.90/0.66 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.90/0.66
% 0.90/0.66 SPASS-SCL-FOL Statistics:
% 0.90/0.66 Number of learned clauses: 23
% 0.90/0.66 Number of propagations: 414
% 0.90/0.66 Number of decisions: 1007
% 0.90/0.66 Number of resolutions: 34
% 0.90/0.66 Number of condensations: 1
% 0.90/0.66 Number of sub resolutions: 1
% 0.90/0.66 Number of input literals (deduplicated): 20
% 0.90/0.66 Number of grows: 10
% 0.90/0.66 Number of considered ground atoms: 224
% 0.90/0.66
% 0.90/0.66 Needed: 0:00:00.14
% 0.90/0.66
%------------------------------------------------------------------------------