The cat eats the cow. The cow likes the cat. If the cat visits the cow then the cat eats the cow. If something is round and nice then it visits the cow. If something eats the cow then the cow visits the cat. All young, round things are nice. If something eats the cow then the cow visits the cat. If something visits the cow then it is kind.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
If the cat visits the cow then the cat eats the cow.
((("cat" "visits" "cow" "+")) -> ("cat" "eats" "cow" "+"))
If something is round and nice then it visits the cow.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "visits" "cow" "+"))
If something eats the cow then the cow visits the cat.
((("something" "eats" "cow" "+")) -> ("cow" "visits" "cat" "+"))
All young, round things are nice.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something eats the cow then the cow visits the cat.
((("something" "eats" "cow" "+")) -> ("cow" "visits" "cat" "+"))
If something visits the cow then it is kind.
((("something" "visits" "cow" "+")) -> ("something" "is" "kind" "+"))
The cat eats the cow.
True
1
proof
[(triple1)]
("cat" "eats" "cow" "+")
triple1
The cow does not like the cat.
False
1
inv-proof
[(triple2)]
("cow" "likes" "cat" "-")
triple2
The cow visits the cat.
True
2
proof
[(((triple1) -> rule3) OR ((triple1) -> rule5))]
("cow" "visits" "cat" "+")
((triple1) -> (rule3 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
((triple1) -> (rule5 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow does not visit the cat.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple1) -> rule5))]
("cow" "visits" "cat" "-")
((triple1) -> (rule3 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
((triple1) -> (rule5 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow is not kind.
Unknown
inv-rconc
[@2: The cow is kind.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("cow" "is" "kind" "-")
The cat is kind.
Unknown
rconc
[@2: The cat is kind.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("cat" "is" "kind" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The cat likes the cow.
Unknown
random
[@0: The cat likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cow" "+")
@0: The cat eats the cow.[(triple1)] The cow likes the cat.[(triple2)] @1: The cow visits the cat.[(((triple1) -> rule3) OR ((triple1) -> rule5))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cow likes the cat.
("cow" "likes" "cat" "+")
triple2
The cow visits the cat.
("cow" "visits" "cat" "+")
((triple1) -> (rule3 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
((triple1) -> (rule5 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1