The cow eats the tiger. The tiger visits the cow. If the tiger eats the cow and the tiger does not visit the cow then the cow is not green. If something eats the tiger then it is big. If something chases the cow then the cow does not eat the tiger. If something visits the cow and the cow is big then the cow does not chase the tiger. If something visits the cow and it chases the tiger then the tiger does not eat the cow. If the tiger visits the cow and the cow does not chase the tiger then the cow visits the tiger.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If the tiger eats the cow and the tiger does not visit the cow then the cow is not green.
((("tiger" "eats" "cow" "+") ("tiger" "visits" "cow" "~")) -> ("cow" "is" "green" "-"))
If something eats the tiger then it is big.
((("something" "eats" "tiger" "+")) -> ("something" "is" "big" "+"))
If something chases the cow then the cow does not eat the tiger.
((("something" "chases" "cow" "+")) -> ("cow" "eats" "tiger" "-"))
If something visits the cow and the cow is big then the cow does not chase the tiger.
((("something" "visits" "cow" "+") ("cow" "is" "big" "+")) -> ("cow" "chases" "tiger" "-"))
If something visits the cow and it chases the tiger then the tiger does not eat the cow.
((("something" "visits" "cow" "+") ("something" "chases" "tiger" "+")) -> ("tiger" "eats" "cow" "-"))
If the tiger visits the cow and the cow does not chase the tiger then the cow visits the tiger.
((("tiger" "visits" "cow" "+") ("cow" "chases" "tiger" "~")) -> ("cow" "visits" "tiger" "+"))
The tiger visits the cow.
True
1
proof
[(triple2)]
("tiger" "visits" "cow" "+")
triple2
The cow does not eat the tiger.
False
1
inv-proof
[(triple1)]
("cow" "eats" "tiger" "-")
triple1
The cow is big.
True
2
proof
[(((triple1) -> rule2))]
("cow" "is" "big" "+")
((triple1) -> (rule2 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "is" "big" "-")
((triple1) -> (rule2 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow does not chase the tiger.
True
4
proof
[(((triple2 ((triple1) -> rule2)) -> rule4))]
("cow" "chases" "tiger" "-")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow chases the tiger.
False
4
inv-proof
[(((triple2 ((triple1) -> rule2)) -> rule4))]
("cow" "chases" "tiger" "+")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow visits the tiger.
True
6
proof
[(((triple2 ((triple2 ((triple1) -> rule2)) -> rule4)) -> rule6))]
("cow" "visits" "tiger" "+")
((triple2 ((triple2 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow does not visit the tiger.
False
6
inv-proof
[(((triple2 ((triple2 ((triple1) -> rule2)) -> rule4)) -> rule6))]
("cow" "visits" "tiger" "-")
((triple2 ((triple2 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The tiger is not big.
Unknown
inv-rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "big" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The tiger eats the cow.
Unknown
random
[@0: The tiger eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cow" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The cow eats the tiger.[(triple1)] The tiger visits the cow.[(triple2)] @1: The cow is big.[(((triple1) -> rule2))] @2: The cow does not chase the tiger.[(((triple2 ((triple1) -> rule2)) -> rule4))] @3: The cow visits the tiger.[(((triple2 ((triple2 ((triple1) -> rule2)) -> rule4)) -> rule6))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
((triple1) -> (rule2 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
((triple2 ((triple2 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
int2
The cow is big.
("cow" "is" "big" "+")
int3