The cat eats the tiger. The cat is big. The cat is blue. The cat is nice. The cat is rough. The cat is young. The cat needs the tiger. The cat sees the tiger. The tiger does not eat the cat. The tiger is not big. The tiger is not blue. The tiger is nice. The tiger is not rough. The tiger is young. The tiger needs the cat. The tiger sees the cat. If someone is big then they see the cat. If someone needs the cat and they see the cat then they do not eat the tiger. If the tiger is blue then the tiger is rough.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is not rough.
("tiger" "is" "rough" "-")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If someone is big then they see the cat.
((("someone" "is" "big" "+")) -> ("someone" "sees" "cat" "+"))
If someone needs the cat and they see the cat then they do not eat the tiger.
((("someone" "needs" "cat" "+") ("someone" "sees" "cat" "+")) -> ("someone" "eats" "tiger" "-"))
If the tiger is blue then the tiger is rough.
((("tiger" "is" "blue" "+")) -> ("tiger" "is" "rough" "+"))
The cat needs the tiger.
True
1
proof
[(triple7)]
("cat" "needs" "tiger" "+")
triple7
The tiger does not see the cat.
False
1
inv-proof
[(triple16)]
("tiger" "sees" "cat" "-")
triple16
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 cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat eats the tiger.[(triple1)] The cat is big.[(triple2)] The cat is blue.[(triple3)] The cat is nice.[(triple4)] The cat is rough.[(triple5)] The cat is young.[(triple6)] The cat needs the tiger.[(triple7)] The cat sees the tiger.[(triple8)] The tiger does not eat the cat.[(triple9)] The tiger is nice.[(triple12)] The tiger is not big.[(triple10)] The tiger is not blue.[(triple11)] The tiger is not rough.[(triple13)] The tiger is young.[(triple14)] The tiger needs the cat.[(triple15)] The tiger sees the cat.[(triple16)] @1: The cat sees the cat.[(((triple2) -> rule1))] The tiger does not eat the tiger.[(((triple15 triple16) -> rule2))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat is rough.
("cat" "is" "rough" "+")
triple5
The cat is young.
("cat" "is" "young" "+")
triple6
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple7
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple8
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
triple9
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger is not big.
("tiger" "is" "big" "-")
triple10
The tiger is not blue.
("tiger" "is" "blue" "-")
triple11
The tiger is not rough.
("tiger" "is" "rough" "-")
triple13
The tiger is young.
("tiger" "is" "young" "+")
triple14
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple15
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple16
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple2) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The tiger does not eat the tiger.
("tiger" "eats" "tiger" "-")
((triple15 triple16) -> (rule2 % int1))
The tiger does not eat the tiger.
("tiger" "eats" "tiger" "-")
int1