Proved

Step Stats: elapsedTime=0.157; cpuTime=0.0; steps=18; roots=1; inputs=9; hornInputs=6; definiteInputs=5; generalInputs=3; factors=0; premiseLiterals=17; rootLiterals=2; generated=118; predicates=3; functions=2; constants=2; skFunctions=0; skConstants=0; expanded=118; derivations=117; factorizations=0; reductions=0; extensions=118; symIDUnif=0; outOrder=0.9915254; maxQueue=128; nResidual=127; nTooDeep=0; nUnacceptable=11; nXUnacceptable=0; nSubsumed=0; nVacuous=0; proofLength=18

Proof Stats: proved=1; elapsedTime=0.157; cpuTime=0.0; subproofs=1; successes=1; steps=18; roots=1; inputs=9; hornInputs=6; definiteInputs=5; generalInputs=3; factors=0; premiseLiterals=17; rootLiterals=2; generated=118; predicates=3; functions=2; constants=2; skFunctions=0; skConstants=0; expanded=118; derivations=117; factorizations=0; reductions=0; extensions=118; symIDUnif=0; outOrder=0.9915254; maxQueue=128; nResidual=127; nTooDeep=0; nUnacceptable=11; nXUnacceptable=0; nSubsumed=0; nVacuous=0; proofLength=18

Elapsed: 0m1s; User: 0m1.5s; System: 0m0.1s