%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SET011-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 : n007.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:27 PM UTC 2026
% Result : Unsatisfiable 0.48s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET011-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.15/0.34 % Computer : n007.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:02:39 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]
% 0.48/0.57 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57 Execution resolution_2 ended with status: unsatisfiable
% 0.48/0.57 Used heuristic: resolution_2
% 0.48/0.57
% 0.48/0.57 Input Clauses:
% 0.48/0.57
% 0.48/0.57 Predicates: member subset equal_sets intersection difference
% 0.48/0.57 Fol Constants: a b aDb aD_aDb
% 0.48/0.57 Fol Functions: member_of_1_not_of_2 h k
% 0.48/0.57 Problem Properties:
% 0.48/0.57 This is a full first-order problem without equality.
% 0.48/0.57
% 0.48/0.57 After reduction: Problem Properties:
% 0.48/0.57 This is a full first-order problem without equality.
% 0.48/0.57
% 0.48/0.57
% 0.48/0.57 Reduced Input Clauses:
% 0.48/0.57
% 0.48/0.57 Most General Atoms: subset(x1,x0) equal_sets(x1,x0) intersection(x0,x1,x2) difference(x1,x2,x3) member(x0,x3)
% 0.48/0.57
% 0.48/0.57 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: resolution_2 ===
% 0.48/0.57
% 0.48/0.57 === Backtracking. Learning clause 22:2:2:[9.4,3.1,2.2]:TopTop: intersection(x0,x0,x1) -> subset(x0,x1)
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 55
% 0.48/0.57 === Restarting.
% 0.48/0.57 === Backtracking. Learning clause 23:2:1:[14.3,19.1]:Top: member(x0,b),member(x0,aDb) ->
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 55
% 0.48/0.57 === Restarting.
% 0.48/0.57 === Backtracking. Learning clause 24:2:1:[13.1,20.1]:Top: member(x0,aD_aDb) -> member(x0,a)
% 0.48/0.57 === Backtracking. Learning clause 25:1:1:[3.1,2.2]:Top: -> subset(x0,x0)
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 58
% 0.48/0.57 === Restarting.
% 0.48/0.57 === Backtracking. Learning clause 26:2:0:[11.2,21.1]:: -> member(h(a,b,aD_aDb),aD_aDb),member(h(a,b,aD_aDb),b)
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 58
% 0.48/0.57 === Restarting.
% 0.48/0.57 === Backtracking. Learning clause 27:1:1:[6.1,25.1]:Top: -> equal_sets(x0,x0)
% 0.48/0.57 === Clause set with instances from active satisfied. Growing active. New size: 122
% 0.48/0.57 === Backtracking. Learning clause 28:6:6:[14.1,15.3,16.1]:TopTopTopTopTopTop: member(x0,x1),member(x0,x2),difference(x2,x3,x4) -> member(x0,x3),member(k(x5,x4,x1),x5),member(k(x5,x4,x1),x1)
% 0.48/0.57 === Backtracking. Learning clause 29:5:5:[15.3,14.1,13.3,26.1]:TopTopTopTopTop: difference(x0,x1,x2),difference(x3,x2,aD_aDb),difference(x0,x4,aD_aDb) -> member(h(a,b,aD_aDb),x1),member(h(a,b,aD_aDb),b)
% 0.48/0.57 === Backtracking. Learning clause 30:4:5:[10.1,13.2]:TopTopTopTopTop: difference(x0,x1,x2) -> intersection(x3,x4,x2),member(h(x3,x4,x2),x3),member(h(x3,x4,x2),x0)
% 0.48/0.57 === Backtracking. Learning clause 31:6:4:[15.2,19.1,14.1,12.2]:TopTopTopTop: member(h(x0,b,x1),a),member(h(x0,b,x1),x2),difference(x3,aDb,x2),member(h(x0,b,x1),x1),member(h(x0,b,x1),x0) -> intersection(x0,b,x1)
% 0.48/0.57 === Conflict found: 23:2:1:[14.3,19.1]:Top: member(x0,b),member(x0,aDb) -> {x0 -> h(a,b,aD_aDb)}
% 0.48/0.57
% 0.48/0.57 SZS status Unsatisfiable
% 0.48/0.57
% 0.48/0.57 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.57
% 0.48/0.57 SPASS-SCL-FOL Statistics:
% 0.48/0.57 Number of learned clauses: 10
% 0.48/0.57 Number of propagations: 228
% 0.48/0.57 Number of decisions: 190
% 0.48/0.57 Number of resolutions: 22
% 0.48/0.57 Number of condensations: 0
% 0.48/0.57 Number of sub resolutions: 0
% 0.48/0.57 Number of input literals (deduplicated): 16
% 0.48/0.57 Number of grows: 5
% 0.48/0.57 Number of considered ground atoms: 122
% 0.48/0.57
% 0.48/0.57 Needed: 0:00:00.04
% 0.48/0.57
%------------------------------------------------------------------------------