The cat eats the tiger. The cat likes the squirrel. The cat visits the tiger. The squirrel is nice. The tiger is big. The tiger is young. The tiger likes the squirrel. If the tiger likes the squirrel and the squirrel eats the cat then the cat eats the tiger. If someone eats the tiger then they eat the cat. If someone is blue then they do not eat the squirrel. If the tiger does not like the squirrel then the squirrel does not eat the cat. If the cat is not nice and the cat is not young then the cat eats the squirrel. If someone eats the cat then they do not like the tiger.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If the tiger likes the squirrel and the squirrel eats the cat then the cat eats the tiger.
((("tiger" "likes" "squirrel" "+") ("squirrel" "eats" "cat" "+")) -> ("cat" "eats" "tiger" "+"))
If someone eats the tiger then they eat the cat.
((("someone" "eats" "tiger" "+")) -> ("someone" "eats" "cat" "+"))
If someone is blue then they do not eat the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "squirrel" "-"))
If the tiger does not like the squirrel then the squirrel does not eat the cat.
((("tiger" "likes" "squirrel" "~")) -> ("squirrel" "eats" "cat" "-"))
If the cat is not nice and the cat is not young then the cat eats the squirrel.
((("cat" "is" "nice" "~") ("cat" "is" "young" "~")) -> ("cat" "eats" "squirrel" "+"))
If someone eats the cat then they do not like the tiger.
((("someone" "eats" "cat" "+")) -> ("someone" "likes" "tiger" "-"))
The cat eats the tiger.
True
1
proof
[(triple1)]
("cat" "eats" "tiger" "+")
triple1
The tiger is not young.
False
1
inv-proof
[(triple6)]
("tiger" "is" "young" "-")
triple6
The cat eats the cat.
True
2
proof
[(((triple1) -> rule2))]
("cat" "eats" "cat" "+")
((triple1) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat does not eat the cat.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "eats" "cat" "-")
((triple1) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The tiger does not eat the cat.
Unknown
inv-rconc
[@1: The tiger eats the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "eats" "cat" "-")
The cat eats the squirrel.
Unknown
rconc
[@1: The cat eats the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "squirrel" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The cat eats the tiger.[(triple1)] The cat likes the squirrel.[(triple2)] The cat visits the tiger.[(triple3)] The squirrel is nice.[(triple4)] The tiger is big.[(triple5)] The tiger is young.[(triple6)] The tiger likes the squirrel.[(triple7)] @1: The cat eats the cat.[(((triple1) -> rule2))] @2: The cat does not like the tiger.[(((((triple1) -> rule2)) -> rule6))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple3
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger is young.
("tiger" "is" "young" "+")
triple6
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple7
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple1) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat does not like the tiger.
("cat" "likes" "tiger" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat does not like the tiger.
("cat" "likes" "tiger" "-")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2