%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SET007-1 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:32:26 PM UTC 2026
% Result : Unsatisfiable 1.73s 0.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET007-1 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n002.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 13:03:32 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.73/0.87 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.73/0.87 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.73/0.87 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.73/0.87 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.73/0.87 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.73/0.87 Execution resolution_2 ended with status: unsatisfiable
% 1.73/0.87 Used heuristic: resolution_2
% 1.73/0.87
% 1.73/0.87 Input Clauses:
% 1.73/0.87
% 1.73/0.87 Predicates: member subset equal_sets union intersection
% 1.73/0.87 Fol Constants: b c bUc a aIb aIc aI_bUc
% 1.73/0.87 Fol Functions: member_of_1_not_of_2 g h
% 1.73/0.87 Problem Properties:
% 1.73/0.87 This is a full first-order problem without equality.
% 1.73/0.87
% 1.73/0.87 After reduction: Problem Properties:
% 1.73/0.87 This is a full first-order problem without equality.
% 1.73/0.87
% 1.73/0.87
% 1.73/0.87 Reduced Input Clauses:
% 1.73/0.87
% 1.73/0.87 Most General Atoms: subset(x1,x0) equal_sets(x1,x0) union(x0,x1,x2) member(x3,x1) intersection(x0,x1,x2)
% 1.73/0.87
% 1.73/0.87 === Starting SPASS-SCL-FOL A Little Less Naive, considering 44 atoms initially, heuristics mode: resolution_2 ===
% 1.73/0.87
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 44
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Backtracking. Learning clause 24:2:1:[9.1,19.1]:Top: member(x0,c) -> member(x0,bUc)
% 1.73/0.87 === Backtracking. Learning clause 25:2:1:[8.1,19.1]:Top: member(x0,b) -> member(x0,bUc)
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 45
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Backtracking. Learning clause 26:2:1:[13.1,20.1]:Top: member(x0,aIb) -> member(x0,a)
% 1.73/0.87 === Backtracking. Learning clause 27:1:1:[16.1,18.1]:Top: -> intersection(x0,x0,x0)
% 1.73/0.87 === Backtracking. Learning clause 28:1:1:[3.1,2.2]:Top: -> subset(x0,x0)
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 46
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Backtracking. Learning clause 29:2:1:[14.1,21.1]:Top: member(x0,aIc) -> member(x0,c)
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 47
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Backtracking. Learning clause 30:3:1:[15.1,22.1]:Top: member(x0,bUc),member(x0,a) -> member(x0,aI_bUc)
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 111
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 114
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Backtracking. Learning clause 31:2:0:[12.3,23.1]:: member(g(aIb,aIc,aI_bUc),aIc),member(g(aIb,aIc,aI_bUc),aI_bUc) ->
% 1.73/0.87 === Backtracking. Learning clause 32:2:0:[11.3,23.1]:: member(g(aIb,aIc,aI_bUc),aIb),member(g(aIb,aIc,aI_bUc),aI_bUc) ->
% 1.73/0.87 === Backtracking. Learning clause 33:1:1:[11.1,10.2]:Top: -> union(x0,x0,x0)
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 114
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 114
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Backtracking. Learning clause 34:1:1:[6.1,28.1]:Top: -> equal_sets(x0,x0)
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 114
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 178
% 1.73/0.87 === Backtracking. Learning clause 35:3:2:[3.2,6.1]:TopTop: member(member_of_1_not_of_2(x0,x1),x1),subset(x1,x0) -> equal_sets(x1,x0)
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 178
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Backtracking. Learning clause 36:5:5:[14.3,15.2,13.3,32.1]:TopTopTopTopTop: intersection(x0,x1,x2),intersection(x2,x1,aIb),intersection(x2,x3,x4),member(g(aIb,aIc,aI_bUc),x4),member(g(aIb,aIc,aI_bUc),aI_bUc) ->
% 1.73/0.87 === Backtracking. Learning clause 37:5:5:[10.4,9.2]:TopTopTopTopTop: union(x0,x1,x2) -> union(x3,x4,x1),member(g(x3,x4,x1),x3),member(g(x3,x4,x1),x4),member(g(x3,x4,x1),x2)
% 1.73/0.87 === Backtracking. Learning clause 39:7:8:[23.0,38.5,10.3,13.2,36.4,14.2]:TopTopTopTopTopTopTopTop: intersection(x0,x1,aIc),intersection(x2,x3,x4),intersection(x4,x3,aIb),intersection(x4,x5,aI_bUc),intersection(x6,x7,x0) -> member(g(aIb,aIc,aI_bUc),aIb),member(g(aIb,aIc,aI_bUc),x7)
% 1.73/0.87 === Backtracking. Learning clause 40:6:7:[10.3,13.2,13.2]:TopTopTopTopTopTopTop: intersection(x0,x1,x2),intersection(x3,x4,x5) -> union(x6,x2,x5),member(g(x6,x2,x5),x6),member(g(x6,x2,x5),x0),member(g(x6,x2,x5),x3)
% 1.73/0.87 === Conflict found: 40:6:7:[10.3,13.2,13.2]:TopTopTopTopTopTopTop: intersection(x0,x1,x2),intersection(x3,x4,x5) -> union(x6,x2,x5),member(g(x6,x2,x5),x6),member(g(x6,x2,x5),x0),member(g(x6,x2,x5),x3) {x0 -> a, x1 -> c, x2 -> aIc, x3 -> a, x4 -> bUc, x5 -> aI_bUc, x6 -> aIb}
% 1.73/0.87 === Backtracking. Learning clause 41:6:6:[40.4,13.2,23.1]:TopTopTopTopTopTop: intersection(x0,x1,aIc),intersection(x2,x3,aI_bUc),intersection(x4,x5,aIb) -> member(g(aIb,aIc,aI_bUc),x0),member(g(aIb,aIc,aI_bUc),x2),member(g(aIb,aIc,aI_bUc),x4)
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 178
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Backtracking. Learning clause 42:2:3:[9.3,3.1,2.2]:TopTopTop: union(x0,x1,x2) -> subset(x1,x2)
% 1.73/0.87 === Backtracking. Learning clause 43:4:3:[15.1,20.1,14.3]:TopTopTop: member(x0,a),intersection(x1,b,x2),member(x0,x2) -> member(x0,aIb)
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 178
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Conflict found: 40:6:7:[10.3,13.2,13.2]:TopTopTopTopTopTopTop: intersection(x0,x1,x2),intersection(x3,x4,x5) -> union(x6,x2,x5),member(g(x6,x2,x5),x6),member(g(x6,x2,x5),x0),member(g(x6,x2,x5),x3) {x0 -> a, x1 -> c, x2 -> aIc, x3 -> a, x4 -> bUc, x5 -> aI_bUc, x6 -> aIb}
% 1.73/0.87 === Backtracking. Learning clause 44:5:4:[40.4,26.1,23.1]:TopTopTopTop: intersection(x0,x1,aIc),intersection(x2,x3,aI_bUc) -> member(g(aIb,aIc,aI_bUc),x0),member(g(aIb,aIc,aI_bUc),x2),member(g(aIb,aIc,aI_bUc),a)
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 189
% 1.73/0.87 === Restarting.
% 1.73/0.87 === Backtracking. Learning clause 45:3:3:[9.2,24.2]:TopTopTop: union(x0,bUc,x1),member(x2,c) -> member(x2,x1)
% 1.73/0.87 === Backtracking. Learning clause 46:3:2:[1.1,24.2]:TopTop: subset(bUc,x0),member(x1,c) -> member(x1,x0)
% 1.73/0.87 === Clause set with instances from active satisfied. Growing active. New size: 253
% 1.73/0.87 === Backtracking. Learning clause 47:3:1:[9.3,30.1,29.2,19.1]:Top: member(x0,a),member(x0,aIc) -> member(x0,aI_bUc)
% 1.73/0.87 === Backtracking. Learning clause 48:4:2:[14.1,20.1,8.2,30.1,19.1,11.2]:TopTop: member(g(x0,x1,aI_bUc),aIb),member(g(x0,x1,aI_bUc),a),member(g(x0,x1,aI_bUc),x0) -> union(x0,x1,aI_bUc)
% 1.73/0.87 === Conflict found: 47:3:1:[9.3,30.1,29.2,19.1]:Top: member(x0,a),member(x0,aIc) -> member(x0,aI_bUc) {x0 -> g(aIb,aIc,aI_bUc)}
% 1.73/0.87 === Backtracking. Learning clause 49:5:2:[47.2,10.3]:TopTop: member(g(x0,aIc,x1),a) -> member(g(x0,aIc,x1),aI_bUc),union(x0,aIc,x1),member(g(x0,aIc,x1),x0),member(g(x0,aIc,x1),x1)
% 1.73/0.87 === Backtracking. Learning clause 50:2:0:[14.1,22.1,1.1,15.2,20.1,49.2,48.1,23.1]:: subset(bUc,b),member(g(aIb,aIc,aI_bUc),a) ->
% 1.73/0.87 === Backtracking. Learning clause 51:3:0:[13.1,21.1,10.3,23.1]:: -> member(g(aIb,aIc,aI_bUc),a),member(g(aIb,aIc,aI_bUc),aIb),member(g(aIb,aIc,aI_bUc),aI_bUc)
% 1.73/0.87 === Conflict found: 41:6:6:[40.4,13.2,23.1]:TopTopTopTopTopTop: intersection(x0,x1,aIc),intersection(x2,x3,aI_bUc),intersection(x4,x5,aIb) -> member(g(aIb,aIc,aI_bUc),x0),member(g(aIb,aIc,aI_bUc),x2),member(g(aIb,aIc,aI_bUc),x4) {x0 -> a, x1 -> c, x2 -> a, x3 -> bUc, x4 -> a, x5 -> b}
% 1.73/0.87 === Backtracking. Learning clause 52:1:0:[41.2,22.1,21.1,20.1,50.2]:: subset(bUc,b) ->
% 1.73/0.87 === Conflict found: 49:5:2:[47.2,10.3]:TopTop: member(g(x0,aIc,x1),a) -> member(g(x0,aIc,x1),aI_bUc),union(x0,aIc,x1),member(g(x0,aIc,x1),x0),member(g(x0,aIc,x1),x1) {x0 -> aIb, x1 -> aI_bUc}
% 1.73/0.87 === Backtracking. Learning clause 54:2:0:[23.0,53.2,49.4,48.1]:: member(g(aIb,aIc,aI_bUc),a) -> member(g(aIb,aIc,aI_bUc),aI_bUc)
% 1.73/0.87 === Conflict found: 26:2:1:[13.1,20.1]:Top: member(x0,aIb) -> member(x0,a) {x0 -> g(aIb,aIc,aI_bUc)}
% 1.73/0.87 === Backtracking. Learning clause 55:1:0:[26.1,51.2,54.1]:: -> member(g(aIb,aIc,aI_bUc),aI_bUc)
% 1.73/0.87 === Backtracking. Learning clause 57:2:0:[54.1,56.1,7.4,15.2,19.1,14.3,22.1,21.1,15.2,20.1,31.1]:: member(g(aIb,aIc,aI_bUc),a) -> member(g(aIb,aIc,aI_bUc),aIb)
% 1.73/0.87 === Conflict found: 41:6:6:[40.4,13.2,23.1]:TopTopTopTopTopTop: intersection(x0,x1,aIc),intersection(x2,x3,aI_bUc),intersection(x4,x5,aIb) -> member(g(aIb,aIc,aI_bUc),x0),member(g(aIb,aIc,aI_bUc),x2),member(g(aIb,aIc,aI_bUc),x4) {x0 -> a, x1 -> c, x2 -> a, x3 -> bUc, x4 -> a, x5 -> b}
% 1.73/0.87
% 1.73/0.87 SZS status Unsatisfiable
% 1.73/0.87
% 1.73/0.87 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.73/0.87
% 1.73/0.87 SPASS-SCL-FOL Statistics:
% 1.73/0.87 Number of learned clauses: 31
% 1.73/0.87 Number of propagations: 1128
% 1.73/0.87 Number of decisions: 1039
% 1.73/0.87 Number of resolutions: 71
% 1.73/0.87 Number of condensations: 0
% 1.73/0.87 Number of sub resolutions: 3
% 1.73/0.87 Number of input literals (deduplicated): 18
% 1.73/0.87 Number of grows: 15
% 1.73/0.87 Number of considered ground atoms: 253
% 1.73/0.87
% 1.73/0.87 Needed: 0:00:00.32
% 1.73/0.87
%------------------------------------------------------------------------------