The cat chases the cow. The cat eats the cow. The cat is nice. The cat needs the cow. The cow eats the cat. The cow is rough. The cow needs the cat. If something chases the cat and the cat is young then the cat chases the cow. All rough things are kind. If something is nice then it chases the cow.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
If something chases the cat and the cat is young then the cat chases the cow.
((("something" "chases" "cat" "+") ("cat" "is" "young" "+")) -> ("cat" "chases" "cow" "+"))
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is nice then it chases the cow.
((("something" "is" "nice" "+")) -> ("something" "chases" "cow" "+"))
The cow eats the cat.
True
1
proof
[(triple5)]
("cow" "eats" "cat" "+")
triple5
The cow does not need the cat.
False
1
inv-proof
[(triple7)]
("cow" "needs" "cat" "-")
triple7
The cat is not kind.
Unknown
inv-rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "kind" "-")
The cow chases the cat.
Unknown
random
[@0: The cow chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cat" "+")
@0: The cat chases the cow.[(triple1 OR ((triple3) -> rule3))] The cat eats the cow.[(triple2)] The cat is nice.[(triple3)] The cat needs the cow.[(triple4)] The cow eats the cat.[(triple5)] The cow is rough.[(triple6)] The cow needs the cat.[(triple7)] @1: The cow is kind.[(((triple6) -> rule2))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
((triple3) -> (rule3 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat needs the cow.
("cat" "needs" "cow" "+")
triple4
The cow eats the cat.
("cow" "eats" "cat" "+")
triple5
The cow is rough.
("cow" "is" "rough" "+")
triple6
The cow needs the cat.
("cow" "needs" "cat" "+")
triple7
The cow is kind.
("cow" "is" "kind" "+")
((triple6) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1