The cat eats the cow. The cat is round. The cat needs the cow. The cow chases the cat. The cow eats the cat. The cow is red. The cow is young. If something needs the cat and it eats the cow then the cat is round. If something eats the cow then the cow is kind.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
If something needs the cat and it eats the cow then the cat is round.
((("something" "needs" "cat" "+") ("something" "eats" "cow" "+")) -> ("cat" "is" "round" "+"))
If something eats the cow then the cow is kind.
((("something" "eats" "cow" "+")) -> ("cow" "is" "kind" "+"))
The cat needs the cow.
True
1
proof
[(triple3)]
("cat" "needs" "cow" "+")
triple3
The cow does not chase the cat.
False
1
inv-proof
[(triple4)]
("cow" "chases" "cat" "-")
triple4
The cow is kind.
True
2
proof
[(((triple1) -> rule2))]
("cow" "is" "kind" "+")
((triple1) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "is" "kind" "-")
((triple1) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat eats the cow.[(triple1)] The cat is round.[(triple2)] The cat needs the cow.[(triple3)] The cow chases the cat.[(triple4)] The cow eats the cat.[(triple5)] The cow is red.[(triple6)] The cow is young.[(triple7)] @1: The cow is kind.[(((triple1) -> rule2))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
triple2
The cat needs the cow.
("cat" "needs" "cow" "+")
triple3
The cow chases the cat.
("cow" "chases" "cat" "+")
triple4
The cow eats the cat.
("cow" "eats" "cat" "+")
triple5
The cow is red.
("cow" "is" "red" "+")
triple6
The cow is young.
("cow" "is" "young" "+")
triple7
The cow is kind.
("cow" "is" "kind" "+")
((triple1) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1