The cow is nice. The cow visits the squirrel. The cow visits the tiger. The squirrel chases the cow. The squirrel chases the tiger. The squirrel is nice. The squirrel needs the tiger. The squirrel visits the cow. The squirrel visits the tiger. The tiger chases the cow. The tiger chases the squirrel. The tiger is blue. The tiger is cold. The tiger needs the cow. The tiger visits the cow. The tiger visits the squirrel. If the cow visits the tiger and the cow chases the tiger then the cow is red. If something chases the squirrel then the squirrel needs the tiger.
The cow is nice.
("cow" "is" "nice" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If the cow visits the tiger and the cow chases the tiger then the cow is red.
((("cow" "visits" "tiger" "+") ("cow" "chases" "tiger" "+")) -> ("cow" "is" "red" "+"))
If something chases the squirrel then the squirrel needs the tiger.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "needs" "tiger" "+"))
The tiger chases the cow.
True
1
proof
[(triple10)]
("tiger" "chases" "cow" "+")
triple10
The tiger does not chase the squirrel.
False
1
inv-proof
[(triple11)]
("tiger" "chases" "squirrel" "-")
triple11
The cow is not red.
Unknown
inv-rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "red" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is nice.[(triple1)] The cow visits the squirrel.[(triple2)] The cow visits the tiger.[(triple3)] The squirrel chases the cow.[(triple4)] The squirrel chases the tiger.[(triple5)] The squirrel is nice.[(triple6)] The squirrel needs the tiger.[(triple7 OR ((triple11) -> rule2))] The squirrel visits the cow.[(triple8)] The squirrel visits the tiger.[(triple9)] The tiger chases the cow.[(triple10)] The tiger chases the squirrel.[(triple11)] The tiger is blue.[(triple12)] The tiger is cold.[(triple13)] The tiger needs the cow.[(triple14)] The tiger visits the cow.[(triple15)] The tiger visits the squirrel.[(triple16)]
The cow is nice.
("cow" "is" "nice" "+")
triple1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple3
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple4
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple5
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple6
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple7
((triple11) -> (rule2 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple8
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple9
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple10
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple11
The tiger is blue.
("tiger" "is" "blue" "+")
triple12
The tiger is cold.
("tiger" "is" "cold" "+")
triple13
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple14
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple15
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple16