The cat eats the tiger. The cat is round. The cat visits the tiger. The tiger is blue. The tiger is round. The tiger likes the cat. The tiger visits the cat. If someone eats the tiger then the tiger eats the cat. If the cat is round then the cat eats the tiger. Round people are blue. If the tiger likes the cat and the tiger is big then the cat visits the tiger. If someone likes the tiger and the tiger is round then they like the cat. If someone is blue then they like the tiger.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is round.
("cat" "is" "round" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone eats the tiger then the tiger eats the cat.
((("someone" "eats" "tiger" "+")) -> ("tiger" "eats" "cat" "+"))
If the cat is round then the cat eats the tiger.
((("cat" "is" "round" "+")) -> ("cat" "eats" "tiger" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If the tiger likes the cat and the tiger is big then the cat visits the tiger.
((("tiger" "likes" "cat" "+") ("tiger" "is" "big" "+")) -> ("cat" "visits" "tiger" "+"))
If someone likes the tiger and the tiger is round then they like the cat.
((("someone" "likes" "tiger" "+") ("tiger" "is" "round" "+")) -> ("someone" "likes" "cat" "+"))
If someone is blue then they like the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "tiger" "+"))
The tiger likes the cat.
True
1
proof
[(triple6 OR ((((triple4) -> rule6) triple5) -> rule5) OR ((((((triple5) -> rule3)) -> rule6) triple5) -> rule5))]
("tiger" "likes" "cat" "+")
triple6
((((triple4) -> (rule6 % int2)) triple5) -> (rule5 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2)) triple5) -> (rule5 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The cat does not visit the tiger.
False
1
inv-proof
[(triple3)]
("cat" "visits" "tiger" "-")
triple3
The tiger likes the tiger.
True
2
proof
[(((triple4) -> rule6) OR ((((triple5) -> rule3)) -> rule6))]
("tiger" "likes" "tiger" "+")
((triple4) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger does not like the tiger.
False
2
inv-proof
[(((triple4) -> rule6) OR ((((triple5) -> rule3)) -> rule6))]
("tiger" "likes" "tiger" "-")
((triple4) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The cat likes the tiger.
True
3
proof
[(((((triple2) -> rule3)) -> rule6))]
("cat" "likes" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat does not like the tiger.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6))]
("cat" "likes" "tiger" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat eats the tiger.[(triple1 OR ((triple2) -> rule2))] The cat is round.[(triple2)] The cat visits the tiger.[(triple3)] The tiger is blue.[(triple4 OR ((triple5) -> rule3))] The tiger is round.[(triple5)] The tiger likes the cat.[(triple6 OR ((((triple4) -> rule6) triple5) -> rule5) OR ((((((triple5) -> rule3)) -> rule6) triple5) -> rule5))] The tiger visits the cat.[(triple7)] @1: The cat is blue.[(((triple2) -> rule3))] The tiger eats the cat.[(((triple1) -> rule1) OR ((((triple2) -> rule2)) -> rule1))] The tiger likes the tiger.[(((triple4) -> rule6) OR ((((triple5) -> rule3)) -> rule6))] @2: The cat likes the tiger.[(((((triple2) -> rule3)) -> rule6))] @3: The cat likes the cat.[(((((((triple2) -> rule3)) -> rule6) triple5) -> rule5))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
((triple2) -> (rule2 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The cat is round.
("cat" "is" "round" "+")
triple2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple3
The tiger is blue.
("tiger" "is" "blue" "+")
triple4
((triple5) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
triple5
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple6
((((triple4) -> (rule6 % int2)) triple5) -> (rule5 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2)) triple5) -> (rule5 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple7
The cat is blue.
("cat" "is" "blue" "+")
((triple2) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
((triple1) -> (rule1 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple4) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2)) triple5) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3