%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SET010-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 : n018.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 4.22s 1.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET010-1 : TPTP v9.2.1. Released v1.0.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n018.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 13:03:18 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 4.22/1.54 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.22/1.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.22/1.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.22/1.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.22/1.54 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.22/1.54 Execution resolution_2 ended with status: unsatisfiable
% 4.22/1.54 Used heuristic: resolution_2
% 4.22/1.54
% 4.22/1.54 Input Clauses:
% 4.22/1.54
% 4.22/1.54 Predicates: member subset equal_sets union intersection difference
% 4.22/1.54 Fol Constants: a b aIb c cDa cDb cD_aIb
% 4.22/1.54 Fol Functions: member_of_1_not_of_2 g h k
% 4.22/1.54 Problem Properties:
% 4.22/1.54 This is a full first-order problem without equality.
% 4.22/1.54
% 4.22/1.54 After reduction: Problem Properties:
% 4.22/1.54 This is a full first-order problem without equality.
% 4.22/1.54
% 4.22/1.54
% 4.22/1.54 Reduced Input Clauses:
% 4.22/1.54
% 4.22/1.54 Most General Atoms: subset(x1,x0) equal_sets(x1,x0) union(x0,x1,x2) intersection(x0,x1,x2) difference(x1,x2,x3) member(x0,x3)
% 4.22/1.54
% 4.22/1.54 === Starting SPASS-SCL-FOL A Little Less Naive, considering 56 atoms initially, heuristics mode: resolution_2 ===
% 4.22/1.54
% 4.22/1.54 === Backtracking. Learning clause 30:1:1:[2.2,3.1]:Top: -> subset(x0,x0)
% 4.22/1.54 === Backtracking. Learning clause 31:1:1:[16.1,18.1]:Top: -> intersection(x0,x0,x0)
% 4.22/1.54 === Backtracking. Learning clause 32:1:1:[10.2,12.1]:Top: -> union(x0,x0,x0)
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 56
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 33:2:1:[14.1,25.1]:Top: member(x0,aIb) -> member(x0,b)
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 57
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 34:2:1:[19.1,26.1]:Top: member(x0,cDa) -> member(x0,c)
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 58
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 35:2:1:[20.3,27.1]:Top: member(x0,b),member(x0,cDb) ->
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 59
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 36:3:1:[21.2,28.1]:Top: member(x0,c) -> member(x0,cD_aIb),member(x0,aIb)
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 123
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 126
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 37:2:0:[12.3,29.1]:: member(g(cDa,cDb,cD_aIb),cDb),member(g(cDa,cDb,cD_aIb),cD_aIb) ->
% 4.22/1.54 === Backtracking. Learning clause 38:2:0:[11.3,29.1]:: member(g(cDa,cDb,cD_aIb),cDa),member(g(cDa,cDb,cD_aIb),cD_aIb) ->
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 126
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 39:1:1:[6.1,30.1]:Top: -> equal_sets(x0,x0)
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 126
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 40:3:5:[21.1,14.3,20.1]:TopTopTopTopTop: difference(x0,x1,x1),intersection(x2,x0,x3),member(x4,x3) ->
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 126
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 41:3:3:[4.2,1.2]:TopTopTop: equal_sets(x0,x1),member(x2,x0) -> member(x2,x1)
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 190
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 190
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 42:4:4:[16.2,14.1]:TopTopTopTop: member(x0,x1) -> member(h(x2,x3,x1),x1),member(h(x2,x3,x1),x2),member(x0,x3)
% 4.22/1.54 === Backtracking. Learning clause 43:4:6:[20.1,19.3]:TopTopTopTopTopTop: member(x0,x1),difference(x2,x3,x1),difference(x3,x4,x5),member(x0,x5) ->
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 190
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Conflict found: 43:4:6:[20.1,19.3]:TopTopTopTopTopTop: member(x0,x1),difference(x2,x3,x1),difference(x3,x4,x5),member(x0,x5) -> {x0 -> b, x1 -> c, x2 -> a, x3 -> a, x4 -> a, x5 -> c}
% 4.22/1.54 === Backtracking. Learning clause 44:4:6:[43.1,1.3]:TopTopTopTopTopTop: difference(x0,x1,x2),difference(x1,x3,x2),member(x4,x5),subset(x5,x2) ->
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 190
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 45:3:3:[2.1,1.2]:TopTopTop: member(x0,x1) -> member(member_of_1_not_of_2(x1,x2),x1),member(x0,x2)
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 198
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Conflict found: 44:4:6:[43.1,1.3]:TopTopTopTopTopTop: difference(x0,x1,x2),difference(x1,x3,x2),member(x4,x5),subset(x5,x2) -> {x0 -> a, x1 -> a, x2 -> aIb, x3 -> a, x4 -> h(a,a,aIb), x5 -> a}
% 4.22/1.54 === Backtracking. Learning clause 46:4:6:[44.4,4.2]:TopTopTopTopTopTop: difference(x0,x1,x2),difference(x1,x3,x2),member(x4,x5),equal_sets(x5,x2) ->
% 4.22/1.54 === Backtracking. Learning clause 47:3:1:[21.4,33.1,28.1]:Top: member(x0,c) -> member(x0,cD_aIb),member(x0,b)
% 4.22/1.54 === Backtracking. Learning clause 48:3:3:[13.3,33.1]:TopTopTop: intersection(aIb,x0,x1),member(x2,x1) -> member(x2,b)
% 4.22/1.54 === Backtracking. Learning clause 49:3:3:[8.3,33.1]:TopTopTop: union(x0,x1,aIb),member(x2,x0) -> member(x2,b)
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 262
% 4.22/1.54 === Backtracking. Learning clause 50:4:4:[22.1,20.3]:TopTopTopTop: member(x0,x1),member(x0,x2) -> member(k(x3,x1,x2),x3),member(k(x3,x1,x2),x2)
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 268
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 51:3:3:[14.3,34.1]:TopTopTop: intersection(x0,cDa,x1),member(x2,x1) -> member(x2,c)
% 4.22/1.54 === Backtracking. Learning clause 52:3:3:[8.3,34.1]:TopTopTop: union(x0,x1,cDa),member(x2,x0) -> member(x2,c)
% 4.22/1.54 === Backtracking. Learning clause 53:2:2:[20.2,9.3,50.3,13.3,25.1,26.1]:TopTop: union(x0,a,cDa),member(x1,aIb) ->
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 274
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 54:3:2:[16.1,35.2]:TopTop: member(h(x0,x1,cDb),b) -> intersection(x0,x1,cDb),member(h(x0,x1,cDb),x0)
% 4.22/1.54 === Clause set with instances from active satisfied. Growing active. New size: 282
% 4.22/1.54 === Restarting.
% 4.22/1.54 === Backtracking. Learning clause 55:4:2:[14.3,37.2,16.2]:TopTop: member(g(cDa,cDb,cD_aIb),x0),member(g(cDa,cDb,cD_aIb),cDb) -> member(h(x1,cD_aIb,x0),x0),member(h(x1,cD_aIb,x0),x1)
% 4.22/1.54 === Conflict found: 47:3:1:[21.4,33.1,28.1]:Top: member(x0,c) -> member(x0,cD_aIb),member(x0,b) {x0 -> g(cDa,cDb,cD_aIb)}
% 4.22/1.54 === Backtracking. Learning clause 56:1:0:[47.3,35.1,19.3,27.1,37.2]:: member(g(cDa,cDb,cD_aIb),cDb) ->
% 4.22/1.54 === Backtracking. Learning clause 58:1:0:[56.0,57.0,13.2,21.4,20.1,19.3,10.2,29.1,28.1,25.1,26.1]:: -> member(g(cDa,cDb,cD_aIb),cD_aIb)
% 4.22/1.54
% 4.22/1.54 SZS status Unsatisfiable
% 4.22/1.54
% 4.22/1.54 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.22/1.54
% 4.22/1.54 SPASS-SCL-FOL Statistics:
% 4.22/1.54 Number of learned clauses: 28
% 4.22/1.54 Number of propagations: 1911
% 4.22/1.54 Number of decisions: 1629
% 4.22/1.54 Number of resolutions: 56
% 4.22/1.54 Number of condensations: 1
% 4.22/1.54 Number of sub resolutions: 1
% 4.22/1.54 Number of input literals (deduplicated): 22
% 4.22/1.54 Number of grows: 18
% 4.22/1.54 Number of considered ground atoms: 282
% 4.22/1.54
% 4.22/1.54 Needed: 0:00:00.96
% 4.22/1.54
%------------------------------------------------------------------------------