The cat chases the tiger. The cat is green. The cat visits the cow. The cow eats the tiger. The tiger eats the cat. The tiger is blue. The tiger visits the cow. If something visits the cat and it chases the tiger then the cat chases the tiger. If something visits the tiger and it visits the cat then the cat chases the tiger. If something eats the cow then the cow chases the cat. If something chases the tiger then the tiger eats the cow. If the cow chases the tiger then the cow chases the cat. If something visits the cow and it chases the cat then the cat eats the cow. If something chases the cow then it visits the cow. If something chases the cow and it is red then the cow eats the cat.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is green.
("cat" "is" "green" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something visits the cat and it chases the tiger then the cat chases the tiger.
((("something" "visits" "cat" "+") ("something" "chases" "tiger" "+")) -> ("cat" "chases" "tiger" "+"))
If something visits the tiger and it visits the cat then the cat chases the tiger.
((("something" "visits" "tiger" "+") ("something" "visits" "cat" "+")) -> ("cat" "chases" "tiger" "+"))
If something eats the cow then the cow chases the cat.
((("something" "eats" "cow" "+")) -> ("cow" "chases" "cat" "+"))
If something chases the tiger then the tiger eats the cow.
((("something" "chases" "tiger" "+")) -> ("tiger" "eats" "cow" "+"))
If the cow chases the tiger then the cow chases the cat.
((("cow" "chases" "tiger" "+")) -> ("cow" "chases" "cat" "+"))
If something visits the cow and it chases the cat then the cat eats the cow.
((("something" "visits" "cow" "+") ("something" "chases" "cat" "+")) -> ("cat" "eats" "cow" "+"))
If something chases the cow then it visits the cow.
((("something" "chases" "cow" "+")) -> ("something" "visits" "cow" "+"))
If something chases the cow and it is red then the cow eats the cat.
((("something" "chases" "cow" "+") ("something" "is" "red" "+")) -> ("cow" "eats" "cat" "+"))
The tiger is blue.
True
1
proof
[(triple6)]
("tiger" "is" "blue" "+")
triple6
The cat is not green.
False
1
inv-proof
[(triple2)]
("cat" "is" "green" "-")
triple2
The tiger eats the cow.
True
2
proof
[(((triple1) -> rule4))]
("tiger" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The tiger does not eat the cow.
False
2
inv-proof
[(((triple1) -> rule4))]
("tiger" "eats" "cow" "-")
((triple1) -> (rule4 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The cow chases the cat.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("cow" "chases" "cat" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2
The cow does not chase the cat.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("cow" "chases" "cat" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2
The cat does not eat the cow.
Unknown
inv-rconc
[@2: The cat eats the cow.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("cat" "eats" "cow" "-")
The cow visits the cow.
Unknown
rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "visits" "cow" "+")
The cow does not eat the cat.
Unknown
inv-rconc
[@1: The cow eats the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "eats" "cat" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The cat chases the cow.
Unknown
random
[@0: The cat chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cow" "+")
@0: The cat chases the tiger.[(triple1)] The cat is green.[(triple2)] The cat visits the cow.[(triple3)] The cow eats the tiger.[(triple4)] The tiger eats the cat.[(triple5)] The tiger is blue.[(triple6)] The tiger visits the cow.[(triple7)] @1: The tiger eats the cow.[(((triple1) -> rule4))] @2: The cow chases the cat.[(((((triple1) -> rule4)) -> rule3))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat visits the cow.
("cat" "visits" "cow" "+")
triple3
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple4
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple5
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple7
The tiger eats the cow.
("tiger" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
int2