%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SET005-1 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n022.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.04s 0.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET005-1 : TPTP v9.2.1. Released v1.0.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n022.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % 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:03:36 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.04/0.72 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.04/0.72 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.04/0.72 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.04/0.72 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.04/0.72 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.04/0.72 Execution resolution_2 ended with status: unsatisfiable
% 1.04/0.72 Used heuristic: resolution_2
% 1.04/0.72
% 1.04/0.72 Input Clauses:
% 1.04/0.72
% 1.04/0.72 Predicates: member subset equal_sets intersection
% 1.04/0.72 Fol Constants: a b aIb c bIc aIbIc
% 1.04/0.72 Fol Functions: member_of_1_not_of_2 h
% 1.04/0.72 Problem Properties:
% 1.04/0.72 This is a full first-order problem without equality.
% 1.04/0.72
% 1.04/0.72 After reduction: Problem Properties:
% 1.04/0.72 This is a full first-order problem without equality.
% 1.04/0.72
% 1.04/0.72
% 1.04/0.72 Reduced Input Clauses:
% 1.04/0.72
% 1.04/0.72 Most General Atoms: subset(x1,x0) equal_sets(x1,x0) intersection(x0,x1,x2) member(x3,x1)
% 1.04/0.72
% 1.04/0.72 === Starting SPASS-SCL-FOL A Little Less Naive, considering 40 atoms initially, heuristics mode: resolution_2 ===
% 1.04/0.72
% 1.04/0.72 === Backtracking. Learning clause 17:1:1:[10.1,12.1]:Top: -> intersection(x0,x0,x0)
% 1.04/0.72 === Clause set with instances from active satisfied. Growing active. New size: 40
% 1.04/0.72 === Restarting.
% 1.04/0.72 === Backtracking. Learning clause 18:2:1:[7.1,13.1]:Top: member(x0,aIb) -> member(x0,a)
% 1.04/0.72 === Clause set with instances from active satisfied. Growing active. New size: 40
% 1.04/0.72 === Restarting.
% 1.04/0.72 === Backtracking. Learning clause 19:2:1:[8.1,14.1]:Top: member(x0,bIc) -> member(x0,c)
% 1.04/0.72 === Clause set with instances from active satisfied. Growing active. New size: 41
% 1.04/0.72 === Restarting.
% 1.04/0.72 === Backtracking. Learning clause 20:3:1:[9.1,15.1]:Top: member(x0,bIc),member(x0,a) -> member(x0,aIbIc)
% 1.04/0.72 === Clause set with instances from active satisfied. Growing active. New size: 44
% 1.04/0.72 === Restarting.
% 1.04/0.72 === Backtracking. Learning clause 21:2:0:[11.2,16.1]:: -> member(h(aIb,c,aIbIc),aIbIc),member(h(aIb,c,aIbIc),c)
% 1.04/0.72 === Clause set with instances from active satisfied. Growing active. New size: 108
% 1.04/0.72 === Backtracking. Learning clause 22:5:5:[9.3,1.3]:TopTopTopTopTop: intersection(x0,x1,x2),member(x3,x1),member(x3,x4),subset(x4,x0) -> member(x3,x2)
% 1.04/0.72 === Clause set with instances from active satisfied. Growing active. New size: 108
% 1.04/0.72 === Restarting.
% 1.04/0.72 === Backtracking. Learning clause 23:3:3:[8.3,19.1]:TopTopTop: intersection(x0,bIc,x1),member(x2,x1) -> member(x2,c)
% 1.04/0.72 === Conflict found: 23:3:3:[8.3,19.1]:TopTopTop: intersection(x0,bIc,x1),member(x2,x1) -> member(x2,c) {x0 -> a, x1 -> aIbIc, x2 -> h(aIb,c,aIbIc)}
% 1.04/0.72 === Backtracking. Learning clause 24:2:1:[23.2,21.1]:Top: intersection(x0,bIc,aIbIc) -> member(h(aIb,c,aIbIc),c)
% 1.04/0.72 === Clause set with instances from active satisfied. Growing active. New size: 115
% 1.04/0.72 === Restarting.
% 1.04/0.72 === Backtracking. Learning clause 25:1:1:[2.2,3.1]:Top: -> subset(x0,x0)
% 1.04/0.72 === Backtracking. Learning clause 26:4:4:[10.2,8.1]:TopTopTopTop: member(x0,x1) -> member(h(x2,x3,x1),x1),member(h(x2,x3,x1),x2),member(x0,x3)
% 1.04/0.72 === Clause set with instances from active satisfied. Growing active. New size: 115
% 1.04/0.72 === Restarting.
% 1.04/0.72 === Backtracking. Learning clause 27:1:1:[6.1,25.1]:Top: -> equal_sets(x0,x0)
% 1.04/0.72 === Clause set with instances from active satisfied. Growing active. New size: 115
% 1.04/0.72 === Restarting.
% 1.04/0.72 === Backtracking. Learning clause 28:8:7:[12.3,9.4,9.4]:TopTopTopTopTopTopTop: member(h(x0,x1,x2),x1),intersection(x3,x4,x0),member(h(x0,x1,x2),x4),member(h(x0,x1,x2),x3),intersection(x5,x6,x2),member(h(x0,x1,x2),x6),member(h(x0,x1,x2),x5) -> intersection(x0,x1,x2)
% 1.04/0.72 === Backtracking. Learning clause 29:10:10:[9.4,9.2,8.3,12.3,9.4]:TopTopTopTopTopTopTopTopTopTop: intersection(x0,x1,x2),member(h(x3,x4,x5),x1),intersection(x0,x2,x3),intersection(x6,x0,x7),member(h(x3,x4,x5),x7),member(h(x3,x4,x5),x4),intersection(x8,x9,x5),member(h(x3,x4,x5),x9),member(h(x3,x4,x5),x8) -> intersection(x3,x4,x5)
% 1.04/0.72 === Clause set with instances from active satisfied. Growing active. New size: 179
% 1.04/0.72 === Conflict found: 29:10:10:[9.4,9.2,8.3,12.3,9.4]:TopTopTopTopTopTopTopTopTopTop: intersection(x0,x1,x2),member(h(x3,x4,x5),x1),intersection(x0,x2,x3),intersection(x6,x0,x7),member(h(x3,x4,x5),x7),member(h(x3,x4,x5),x4),intersection(x8,x9,x5),member(h(x3,x4,x5),x9),member(h(x3,x4,x5),x8) -> intersection(x3,x4,x5) {x0 -> a, x1 -> c, x2 -> bIc, x3 -> aIb, x4 -> c, x5 -> aIbIc, x6 -> c, x7 -> bIc, x8 -> a, x9 -> bIc}
% 1.04/0.72 === Backtracking. Learning clause 30:12:12:[29.5,22.5]:TopTopTopTopTopTopTopTopTopTopTopTop: intersection(x0,x1,x2),member(h(x3,x4,x5),x1),intersection(x0,x2,x3),intersection(x6,x0,x7),member(h(x3,x4,x5),x4),intersection(x8,x7,x5),member(h(x3,x4,x5),x8),intersection(x9,x10,x7),member(h(x3,x4,x5),x10),member(h(x3,x4,x5),x11),subset(x11,x9) -> intersection(x3,x4,x5)
% 1.04/0.72 === Backtracking. Learning clause 31:7:8:[9.4,22.2,8.3]:TopTopTopTopTopTopTopTop: intersection(x0,x1,x2),member(x3,x0),intersection(x4,x2,x5),subset(x1,x4),intersection(x6,x1,x7),member(x3,x7) -> member(x3,x5)
% 1.04/0.72 === Conflict found: 22:5:5:[9.3,1.3]:TopTopTopTopTop: intersection(x0,x1,x2),member(x3,x1),member(x3,x4),subset(x4,x0) -> member(x3,x2) {x0 -> b, x1 -> c, x2 -> bIc, x3 -> h(aIb,c,aIbIc), x4 -> b}
% 1.04/0.72 === Backtracking. Learning clause 32:10:12:[22.3,8.3,22.2,7.3,10.3]:TopTopTopTopTopTopTopTopTopTopTopTop: intersection(x0,x1,x2),member(h(x3,x4,x5),x1),subset(x6,x0),intersection(x7,x6,x3),intersection(x8,x2,x9),subset(x10,x8),intersection(x10,x11,x3) -> member(h(x3,x4,x5),x9),member(h(x3,x4,x5),x5),intersection(x3,x4,x5)
% 1.04/0.72 === Conflict found: 22:5:5:[9.3,1.3]:TopTopTopTopTop: intersection(x0,x1,x2),member(x3,x1),member(x3,x4),subset(x4,x0) -> member(x3,x2) {x0 -> a, x1 -> b, x2 -> aIb, x3 -> h(aIb,c,aIbIc), x4 -> a}
% 1.04/0.72
% 1.04/0.72 SZS status Unsatisfiable
% 1.04/0.72
% 1.04/0.72 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.04/0.72
% 1.04/0.72 SPASS-SCL-FOL Statistics:
% 1.04/0.72 Number of learned clauses: 16
% 1.04/0.72 Number of propagations: 550
% 1.04/0.72 Number of decisions: 450
% 1.04/0.72 Number of resolutions: 36
% 1.04/0.72 Number of condensations: 0
% 1.04/0.72 Number of sub resolutions: 0
% 1.04/0.72 Number of input literals (deduplicated): 13
% 1.04/0.72 Number of grows: 10
% 1.04/0.72 Number of considered ground atoms: 179
% 1.04/0.72
% 1.04/0.72 Needed: 0:00:00.17
% 1.04/0.72
%------------------------------------------------------------------------------