The cat eats the cow. The cat eats the rabbit. The cat is kind. The cat is red. The cat is round. The cat needs the cow. The cat needs the rabbit. The cow eats the cat. The cow needs the cat. The cow needs the rabbit. The rabbit eats the cow. The rabbit needs the cat. If someone visits the cat then the cat eats the cow. If someone visits the cat and they are round then the cat is red. If someone is kind then they eat the rabbit. If someone is nice then they need the cow. If the rabbit eats the cow then the cow is kind. If someone needs the cow then the cow needs the rabbit.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If someone visits the cat then the cat eats the cow.
((("someone" "visits" "cat" "+")) -> ("cat" "eats" "cow" "+"))
If someone visits the cat and they are round then the cat is red.
((("someone" "visits" "cat" "+") ("someone" "is" "round" "+")) -> ("cat" "is" "red" "+"))
If someone is kind then they eat the rabbit.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is nice then they need the cow.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "cow" "+"))
If the rabbit eats the cow then the cow is kind.
((("rabbit" "eats" "cow" "+")) -> ("cow" "is" "kind" "+"))
If someone needs the cow then the cow needs the rabbit.
((("someone" "needs" "cow" "+")) -> ("cow" "needs" "rabbit" "+"))
The rabbit eats the cow.
True
1
proof
[(triple11)]
("rabbit" "eats" "cow" "+")
triple11
The cat does not eat the rabbit.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule3))]
("cat" "eats" "rabbit" "-")
triple2
((triple3) -> (rule3 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat eats the cow.[(triple1)] The cat eats the rabbit.[(triple2 OR ((triple3) -> rule3))] The cat is kind.[(triple3)] The cat is red.[(triple4)] The cat is round.[(triple5)] The cat needs the cow.[(triple6)] The cat needs the rabbit.[(triple7)] The cow eats the cat.[(triple8)] The cow needs the cat.[(triple9)] The cow needs the rabbit.[(triple10 OR ((triple6) -> rule6))] The rabbit eats the cow.[(triple11)] The rabbit needs the cat.[(triple12)] @1: The cow is kind.[(((triple11) -> rule5))] @2: The cow eats the rabbit.[(((((triple11) -> rule5)) -> rule3))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple2
((triple3) -> (rule3 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The cat needs the cow.
("cat" "needs" "cow" "+")
triple6
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple7
The cow eats the cat.
("cow" "eats" "cat" "+")
triple8
The cow needs the cat.
("cow" "needs" "cat" "+")
triple9
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple10
((triple6) -> (rule6 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple11
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple12
The cow is kind.
("cow" "is" "kind" "+")
((triple11) -> (rule5 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
((((triple11) -> (rule5 % int2))) -> (rule3 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2