The cow does not visit the squirrel. The squirrel is big. The squirrel is nice. The squirrel is red. The squirrel does not see the tiger. The tiger does not need the cow. The tiger needs the squirrel. If something is blue and big then it visits the cow. Nice things are red. Round things are big.
The cow does not visit the squirrel.
("cow" "visits" "squirrel" "-")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
The tiger does not need the cow.
("tiger" "needs" "cow" "-")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If something is blue and big then it visits the cow.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "visits" "cow" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
The tiger does not need the cow.
True
1
proof
[(triple6)]
("tiger" "needs" "cow" "-")
triple6
The cow visits the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "visits" "squirrel" "+")
triple1
The tiger does not visit the cow.
Unknown
inv-rconc
[@1: The tiger visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "cow" "-")
The squirrel needs the cow.
Unknown
random
[@0: The squirrel needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cow" "+")
@0: The cow does not visit the squirrel.[(triple1)] The squirrel does not see the tiger.[(triple5)] The squirrel is big.[(triple2)] The squirrel is nice.[(triple3)] The squirrel is red.[(triple4 OR ((triple3) -> rule2))] The tiger does not need the cow.[(triple6)] The tiger needs the squirrel.[(triple7)]
The cow does not visit the squirrel.
("cow" "visits" "squirrel" "-")
triple1
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
triple5
The squirrel is big.
("squirrel" "is" "big" "+")
triple2
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple3
The squirrel is red.
("squirrel" "is" "red" "+")
triple4
((triple3) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The tiger does not need the cow.
("tiger" "needs" "cow" "-")
triple6
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple7