The cow eats the tiger. The cow is red. The cow is round. The cow needs the squirrel. The cow does not need the tiger. The cow does not visit the tiger. The squirrel eats the tiger. The squirrel is not green. The squirrel is red. The tiger is nice. The tiger needs the cow. The tiger needs the squirrel. If the tiger needs the squirrel and the squirrel is not green then the squirrel needs the tiger. If someone visits the tiger and the tiger eats the cow then they visit the cow. If someone eats the squirrel then they are red.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The cow does not need the tiger.
("cow" "needs" "tiger" "-")
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is not green.
("squirrel" "is" "green" "-")
The squirrel is red.
("squirrel" "is" "red" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If the tiger needs the squirrel and the squirrel is not green then the squirrel needs the tiger.
((("tiger" "needs" "squirrel" "+") ("squirrel" "is" "green" "~")) -> ("squirrel" "needs" "tiger" "+"))
If someone visits the tiger and the tiger eats the cow then they visit the cow.
((("someone" "visits" "tiger" "+") ("tiger" "eats" "cow" "+")) -> ("someone" "visits" "cow" "+"))
If someone eats the squirrel then they are red.
((("someone" "eats" "squirrel" "+")) -> ("someone" "is" "red" "+"))
The cow is red.
True
1
proof
[(triple2)]
("cow" "is" "red" "+")
triple2
The cow does not need the squirrel.
False
1
inv-proof
[(triple4)]
("cow" "needs" "squirrel" "-")
triple4
The squirrel needs the tiger.
True
3
proof
[(((triple12 triple8) -> rule1))]
("squirrel" "needs" "tiger" "+")
((triple12 triple8) -> (rule1 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel does not need the tiger.
False
3
inv-proof
[(((triple12 triple8) -> rule1))]
("squirrel" "needs" "tiger" "-")
((triple12 triple8) -> (rule1 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel does not visit the cow.
Unknown
inv-rconc
[@1: The squirrel visits the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "cow" "-")
The tiger is red.
Unknown
rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "red" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The cow does not need the tiger.[(triple5)] The cow does not visit the tiger.[(triple6)] The cow eats the tiger.[(triple1)] The cow is red.[(triple2)] The cow is round.[(triple3)] The cow needs the squirrel.[(triple4)] The squirrel eats the tiger.[(triple7)] The squirrel is not green.[(triple8)] The squirrel is red.[(triple9)] The tiger is nice.[(triple10)] The tiger needs the cow.[(triple11)] The tiger needs the squirrel.[(triple12)] @1: The squirrel needs the tiger.[(((triple12 triple8) -> rule1))]
The cow does not need the tiger.
("cow" "needs" "tiger" "-")
triple5
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
triple6
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The cow is round.
("cow" "is" "round" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple4
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple7
The squirrel is not green.
("squirrel" "is" "green" "-")
triple8
The squirrel is red.
("squirrel" "is" "red" "+")
triple9
The tiger is nice.
("tiger" "is" "nice" "+")
triple10
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple11
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple12
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
((triple12 triple8) -> (rule1 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1