%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : PUZ028-3 : TPTP v9.2.1. Released v1.1.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/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:31:26 PM UTC 2026 % Result : Satisfiable 0.31s 0.57s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : PUZ028-3 : TPTP v9.2.1. Released v1.1.0. % 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.31 % Computer : n007.cluster.edu % 0.13/0.31 % Model : x86_64 x86_64 % 0.13/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.31 % Memory : 8042.1875MB % 0.13/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.31 % CPULimit : 300 % 0.13/0.31 % WCLimit : 300 % 0.13/0.31 % DateTime : Thu May 7 12:56:54 EDT 2026 % 0.13/0.32 % CPUTime : % 0.13/0.32 SPASS-SCL-FOL version: % 0.21/0.41 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.31/0.57 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.31/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.31/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.31/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.31/0.57 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.31/0.57 Execution normal ended with status: satisfiable % 0.31/0.57 Used heuristic: normal % 0.31/0.57 % 0.31/0.57 Input Clauses: % 0.31/0.57 % 0.31/0.57 Predicates: person not_equal familiar not_familiar % 0.31/0.57 Fol Constants: n1 n2 n3 n4 n5 n6 % 0.31/0.57 Fol Functions: % 0.31/0.57 Problem Properties: % 0.31/0.57 This is a first-order ground problem without equality. % 0.31/0.57 % 0.31/0.57 After reduction: Problem Properties: % 0.31/0.57 This is a first-order ground problem without equality. % 0.31/0.57 % 0.31/0.57 % 0.31/0.57 Reduced Input Clauses: % 0.31/0.57 507:1:0:[1.0,37.0,73.0,505.2,289.0,506.3]:: not_equal(n1,n1) -> % 0.31/0.57 510:2:0:[1.0,38.0,2.0,508.1,7.0,509.2]:: -> familiar(n1,n2),not_familiar(n1,n2) % 0.31/0.57 513:2:0:[1.0,39.0,3.0,511.1,8.0,512.2]:: -> familiar(n1,n3),not_familiar(n1,n3) % 0.31/0.57 516:2:0:[1.0,40.0,4.0,514.1,9.0,515.2]:: -> familiar(n1,n4),not_familiar(n1,n4) % 0.31/0.57 519:2:0:[1.0,41.0,5.0,517.1,10.0,518.2]:: -> familiar(n1,n5),not_familiar(n1,n5) % 0.31/0.57 522:2:0:[1.0,42.0,6.0,520.1,11.0,521.2]:: -> familiar(n1,n6),not_familiar(n1,n6) % 0.31/0.57 525:2:0:[2.0,43.0,1.0,523.1,12.0,524.2]:: -> familiar(n2,n1),not_familiar(n2,n1) % 0.31/0.57 528:1:0:[2.0,44.0,116.0,526.2,332.0,527.3]:: not_equal(n2,n2) -> % 0.31/0.57 531:2:0:[2.0,45.0,3.0,529.1,13.0,530.2]:: -> familiar(n2,n3),not_familiar(n2,n3) % 0.31/0.57 534:2:0:[2.0,46.0,4.0,532.1,14.0,533.2]:: -> familiar(n2,n4),not_familiar(n2,n4) % 0.31/0.57 537:2:0:[2.0,47.0,5.0,535.1,15.0,536.2]:: -> familiar(n2,n5),not_familiar(n2,n5) % 0.31/0.57 540:2:0:[2.0,48.0,6.0,538.1,16.0,539.2]:: -> familiar(n2,n6),not_familiar(n2,n6) % 0.31/0.57 543:2:0:[3.0,49.0,1.0,541.1,17.0,542.2]:: -> familiar(n3,n1),not_familiar(n3,n1) % 0.31/0.57 546:2:0:[3.0,50.0,2.0,544.1,18.0,545.2]:: -> familiar(n3,n2),not_familiar(n3,n2) % 0.31/0.57 549:1:0:[3.0,51.0,159.0,547.2,375.0,548.3]:: not_equal(n3,n3) -> % 0.31/0.57 552:2:0:[3.0,52.0,4.0,550.1,19.0,551.2]:: -> familiar(n3,n4),not_familiar(n3,n4) % 0.31/0.57 555:2:0:[3.0,53.0,5.0,553.1,20.0,554.2]:: -> familiar(n3,n5),not_familiar(n3,n5) % 0.31/0.57 558:2:0:[3.0,54.0,6.0,556.1,21.0,557.2]:: -> familiar(n3,n6),not_familiar(n3,n6) % 0.31/0.57 561:2:0:[4.0,55.0,1.0,559.1,22.0,560.2]:: -> familiar(n4,n1),not_familiar(n4,n1) % 0.31/0.57 564:2:0:[4.0,56.0,2.0,562.1,23.0,563.2]:: -> familiar(n4,n2),not_familiar(n4,n2) % 0.31/0.57 567:2:0:[4.0,57.0,3.0,565.1,24.0,566.2]:: -> familiar(n4,n3),not_familiar(n4,n3) % 0.31/0.57 570:1:0:[4.0,58.0,202.0,568.2,418.0,569.3]:: not_equal(n4,n4) -> % 0.31/0.57 573:2:0:[4.0,59.0,5.0,571.1,25.0,572.2]:: -> familiar(n4,n5),not_familiar(n4,n5) % 0.31/0.57 576:2:0:[4.0,60.0,6.0,574.1,26.0,575.2]:: -> familiar(n4,n6),not_familiar(n4,n6) % 0.31/0.57 579:2:0:[5.0,61.0,1.0,577.1,27.0,578.2]:: -> familiar(n5,n1),not_familiar(n5,n1) % 0.31/0.57 582:2:0:[5.0,62.0,2.0,580.1,28.0,581.2]:: -> familiar(n5,n2),not_familiar(n5,n2) % 0.31/0.57 585:2:0:[5.0,63.0,3.0,583.1,29.0,584.2]:: -> familiar(n5,n3),not_familiar(n5,n3) % 0.31/0.57 588:2:0:[5.0,64.0,4.0,586.1,30.0,587.2]:: -> familiar(n5,n4),not_familiar(n5,n4) % 0.31/0.57 591:1:0:[5.0,65.0,245.0,589.2,461.0,590.3]:: not_equal(n5,n5) -> % 0.31/0.57 594:2:0:[5.0,66.0,6.0,592.1,31.0,593.2]:: -> familiar(n5,n6),not_familiar(n5,n6) % 0.31/0.57 597:2:0:[6.0,67.0,1.0,595.1,32.0,596.2]:: -> familiar(n6,n1),not_familiar(n6,n1) % 0.31/0.57 600:2:0:[6.0,68.0,2.0,598.1,33.0,599.2]:: -> familiar(n6,n2),not_familiar(n6,n2) % 0.31/0.57 603:2:0:[6.0,69.0,3.0,601.1,34.0,602.2]:: -> familiar(n6,n3),not_familiar(n6,n3) % 0.31/0.57 606:2:0:[6.0,70.0,4.0,604.1,35.0,605.2]:: -> familiar(n6,n4),not_familiar(n6,n4) % 0.31/0.57 609:2:0:[6.0,71.0,5.0,607.1,36.0,608.2]:: -> familiar(n6,n5),not_familiar(n6,n5) % 0.31/0.57 612:1:0:[6.0,72.0,288.0,610.2,504.0,611.3]:: not_equal(n6,n6) -> % 0.31/0.57 % 0.31/0.57 Most General Atoms: person(n1) person(n2) person(n3) person(n4) person(n5) person(n6) not_equal(n1,n2) not_equal(n1,n3) not_equal(n1,n4) not_equal(n1,n5) not_equal(n1,n6) not_equal(n2,n1) not_equal(n2,n3) not_equal(n2,n4) not_equal(n2,n5) not_equal(n2,n6) not_equal(n3,n1) not_equal(n3,n2) not_equal(n3,n4) not_equal(n3,n5) not_equal(n3,n6) not_equal(n4,n1) not_equal(n4,n2) not_equal(n4,n3) not_equal(n4,n5) not_equal(n4,n6) not_equal(n5,n1) not_equal(n5,n2) not_equal(n5,n3) not_equal(n5,n4) not_equal(n5,n6) not_equal(n6,n1) not_equal(n6,n2) not_equal(n6,n3) not_equal(n6,n4) not_equal(n6,n5) not_equal(n1,n1) familiar(n1,n2) not_familiar(n1,n2) familiar(n1,n3) not_familiar(n1,n3) familiar(n1,n4) not_familiar(n1,n4) familiar(n1,n5) not_familiar(n1,n5) familiar(n1,n6) not_familiar(n1,n6) familiar(n2,n1) not_familiar(n2,n1) not_equal(n2,n2) familiar(n2,n3) not_familiar(n2,n3) familiar(n2,n4) not_familiar(n2,n4) familiar(n2,n5) not_familiar(n2,n5) familiar(n2,n6) not_familiar(n2,n6) familiar(n3,n1) not_familiar(n3,n1) familiar(n3,n2) not_familiar(n3,n2) not_equal(n3,n3) familiar(n3,n4) not_familiar(n3,n4) familiar(n3,n5) not_familiar(n3,n5) familiar(n3,n6) not_familiar(n3,n6) familiar(n4,n1) not_familiar(n4,n1) familiar(n4,n2) not_familiar(n4,n2) familiar(n4,n3) not_familiar(n4,n3) not_equal(n4,n4) familiar(n4,n5) not_familiar(n4,n5) familiar(n4,n6) not_familiar(n4,n6) familiar(n5,n1) not_familiar(n5,n1) familiar(n5,n2) not_familiar(n5,n2) familiar(n5,n3) not_familiar(n5,n3) familiar(n5,n4) not_familiar(n5,n4) not_equal(n5,n5) familiar(n5,n6) not_familiar(n5,n6) familiar(n6,n1) not_familiar(n6,n1) familiar(n6,n2) not_familiar(n6,n2) familiar(n6,n3) not_familiar(n6,n3) familiar(n6,n4) not_familiar(n6,n4) familiar(n6,n5) not_familiar(n6,n5) not_equal(n6,n6) familiar(n1,n1) not_familiar(n6,n6) not_familiar(n5,n5) not_familiar(n4,n4) not_familiar(n3,n3) familiar(n2,n2) not_familiar(n2,n2) not_familiar(n1,n1) familiar(n6,n6) familiar(n5,n5) familiar(n4,n4) familiar(n3,n3) % 0.31/0.57 % 0.31/0.57 === Starting SPASS-SCL-FOL A Little Less Naive, considering 114 atoms initially, heuristics mode: normal === % 0.31/0.57 % 0.31/0.57 % 0.31/0.57 Linear Model Building succeeded. % 0.31/0.57 SZS status Satisfiable % 0.31/0.57 % 0.31/0.57 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.31/0.57 % 0.31/0.57 SPASS-SCL-FOL Statistics: % 0.31/0.57 Number of learned clauses: 0 % 0.31/0.57 Number of propagations: 97 % 0.31/0.57 Number of decisions: 17 % 0.31/0.57 Number of resolutions: 0 % 0.31/0.57 Number of condensations: 0 % 0.31/0.57 Number of sub resolutions: 108 % 0.31/0.57 Number of input literals (deduplicated): 114 % 0.31/0.57 Number of grows: 0 % 0.31/0.57 Number of considered ground atoms: 114 % 0.31/0.57 % 0.31/0.57 Needed: 0:00:00.01 % 0.31/0.57 %------------------------------------------------------------------------------