The cow eats the tiger. The cow is red. The cow is rough. The cow is round. The cow likes the tiger. The cow does not visit the tiger. The tiger eats the cow. The tiger is big. The tiger is rough. The tiger is round. The tiger does not like the cow. The tiger visits the cow. If the tiger is not cold then the tiger likes the cow. If something eats the tiger and it visits the cow then it is round. If something is big then it visits the tiger. If something is red and not big then it is rough. If something likes the cow and the cow is not big then the cow does not like the tiger. If something eats the tiger and the tiger visits the cow then it visits the cow. If the cow is rough and the cow does not like the tiger then the cow is not round. If the tiger does not visit the cow then the tiger is not round.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is round.
("cow" "is" "round" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If the tiger is not cold then the tiger likes the cow.
((("tiger" "is" "cold" "~")) -> ("tiger" "likes" "cow" "+"))
If something eats the tiger and it visits the cow then it is round.
((("something" "eats" "tiger" "+") ("something" "visits" "cow" "+")) -> ("something" "is" "round" "+"))
If something is big then it visits the tiger.
((("something" "is" "big" "+")) -> ("something" "visits" "tiger" "+"))
If something is red and not big then it is rough.
((("something" "is" "red" "+") ("something" "is" "big" "~")) -> ("something" "is" "rough" "+"))
If something likes the cow and the cow is not big then the cow does not like the tiger.
((("something" "likes" "cow" "+") ("cow" "is" "big" "~")) -> ("cow" "likes" "tiger" "-"))
If something eats the tiger and the tiger visits the cow then it visits the cow.
((("something" "eats" "tiger" "+") ("tiger" "visits" "cow" "+")) -> ("something" "visits" "cow" "+"))
If the cow is rough and the cow does not like the tiger then the cow is not round.
((("cow" "is" "rough" "+") ("cow" "likes" "tiger" "~")) -> ("cow" "is" "round" "-"))
If the tiger does not visit the cow then the tiger is not round.
((("tiger" "visits" "cow" "~")) -> ("tiger" "is" "round" "-"))
The cow eats the tiger.
True
1
proof
[(triple1)]
("cow" "eats" "tiger" "+")
triple1
The cow does not eat the tiger.
False
1
inv-proof
[(triple1)]
("cow" "eats" "tiger" "-")
triple1
The tiger visits the tiger.
True
2
proof
[(((triple8) -> rule3))]
("tiger" "visits" "tiger" "+")
((triple8) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple8) -> rule3))]
("tiger" "visits" "tiger" "-")
((triple8) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow does not visit the tiger.[(triple6)] The cow eats the tiger.[(triple1)] The cow is red.[(triple2)] The cow is rough.[(triple3)] The cow is round.[(triple4 OR ((triple1 ((triple1 triple12) -> rule6)) -> rule2))] The cow likes the tiger.[(triple5)] The tiger does not like the cow.[(triple11)] The tiger eats the cow.[(triple7)] The tiger is big.[(triple8)] The tiger is rough.[(triple9)] The tiger is round.[(triple10)] The tiger visits the cow.[(triple12)] @1: The cow visits the cow.[(((triple1 triple12) -> rule6))] The tiger visits the tiger.[(((triple8) -> rule3))]
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 rough.
("cow" "is" "rough" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
((triple1 ((triple1 triple12) -> (rule6 % int2))) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple5
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
triple11
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple7
The tiger is big.
("tiger" "is" "big" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple12
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple1 triple12) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple8) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1