The cat eats the cow. The cow eats the cat. If someone needs the cow and the cow needs the cat then they eat the cat. If someone needs the cow then the cow is blue. If someone eats the cat then they need the cow.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
If someone needs the cow and the cow needs the cat then they eat the cat.
((("someone" "needs" "cow" "+") ("cow" "needs" "cat" "+")) -> ("someone" "eats" "cat" "+"))
If someone needs the cow then the cow is blue.
((("someone" "needs" "cow" "+")) -> ("cow" "is" "blue" "+"))
If someone eats the cat then they need the cow.
((("someone" "eats" "cat" "+")) -> ("someone" "needs" "cow" "+"))
The cat eats the cow.
True
1
proof
[(triple1)]
("cat" "eats" "cow" "+")
triple1
The cow does not eat the cat.
False
1
inv-proof
[(triple2)]
("cow" "eats" "cat" "-")
triple2
The cow needs the cow.
True
2
proof
[(((triple2) -> rule3))]
("cow" "needs" "cow" "+")
((triple2) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple2) -> rule3))]
("cow" "needs" "cow" "-")
((triple2) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is blue.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("cow" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is not blue.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("cow" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cat does not need the cow.
Unknown
inv-rconc
[@2: The cat needs the cow.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("cat" "needs" "cow" "-")
The cat eats the cat.
Unknown
rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "cat" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
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 needs the cat.
Unknown
random
[@0: The cow needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cat" "+")
@0: The cat eats the cow.[(triple1)] The cow eats the cat.[(triple2)] @1: The cow needs the cow.[(((triple2) -> rule3))] @2: The cow is blue.[(((((triple2) -> rule3)) -> rule2))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cow eats the cat.
("cow" "eats" "cat" "+")
triple2
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple2) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2