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