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