4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa content { '--------------------------SPASS-START-----------------------------
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen KuksaInput Problem:
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa1[0:Inp] || equal(skc1,skc1)* -> .
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa This is a unit equality problem.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa This is a problem that has, if any, a finite domain model.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa There are no function symbols.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa The conjecture is ground.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa Axiom clauses: 0 Conjecture clauses: 1
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa Inferences: IEqR=1
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa Reductions: RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RFSub=1 RBSub=1
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa Extras : Input Saturation, Always Selection, No Splitting, Full Reduction, Ratio: 5, FuncWeight: 1, VarWeight: 1
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa Precedence: skc0 > skc1
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa Ordering : KBO
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen KuksaProcessed Problem:
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen KuksaWorked Off Clauses:
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen KuksaUsable Clauses:
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen KuksaSPASS beiseite: Proof found.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen KuksaProblem: Read from stdin.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen KuksaSPASS derived 0 clauses, backtracked 0 clauses, performed 0 splits and kept 1 clauses.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen KuksaSPASS allocated 45930 KBytes.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen KuksaSPASS spent 0:00:00.03 on the problem.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa 0:00:00.01 for the input.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa 0:00:00.01 for the FLOTTER CNF translation.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa 0:00:00.00 for inferences.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa 0:00:00.00 for the backtracking.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa 0:00:00.00 for the reduction.
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen KuksaHere is a proof with depth 0, length 2 :
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa1[0:Inp] || equal(skc1,skc1)* -> .
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa2[0:Obv:1.0] || -> .
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen KuksaFormulae used in the proof : ax1
4a7c98053955ca61668ed12b235ddf2fc9976142Eugen Kuksa--------------------------SPASS-STOP------------------------------' }