The cat eats the rabbit. The cat is not big. The cat needs the dog. The cat needs the lion. The cat sees the rabbit. The dog eats the cat. The dog is big. The dog is red. The lion does not eat the cat. The rabbit sees the lion. If something sees the lion and it sees the rabbit then the rabbit eats the cat. If something eats the cat then it is not round. If something needs the dog and it is not blue then the dog eats the lion.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is not big.
("cat" "is" "big" "-")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is red.
("dog" "is" "red" "+")
The lion does not eat the cat.
("lion" "eats" "cat" "-")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If something sees the lion and it sees the rabbit then the rabbit eats the cat.
((("something" "sees" "lion" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "eats" "cat" "+"))
If something eats the cat then it is not round.
((("something" "eats" "cat" "+")) -> ("something" "is" "round" "-"))
If something needs the dog and it is not blue then the dog eats the lion.
((("something" "needs" "dog" "+") ("something" "is" "blue" "~")) -> ("dog" "eats" "lion" "+"))
The dog is red.
True
1
proof
[(triple8)]
("dog" "is" "red" "+")
triple8
The dog is not big.
False
1
inv-proof
[(triple7)]
("dog" "is" "big" "-")
triple7
The dog is not round.
True
2
proof
[(((triple6) -> rule2))]
("dog" "is" "round" "-")
((triple6) -> (rule2 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The dog is round.
False
2
inv-proof
[(((triple6) -> rule2))]
("dog" "is" "round" "+")
((triple6) -> (rule2 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The dog does not eat the lion.
Unknown
inv-rconc
[@1: The dog eats the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "eats" "lion" "-")
The rabbit eats the cat.
Unknown
rconc
[@1: The rabbit eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "cat" "+")
The dog does not see the rabbit.
Unknown
inv-random
[@0: The dog sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "rabbit" "-")
The dog needs the cat.
Unknown
random
[@0: The dog needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cat" "+")
@0: The cat eats the rabbit.[(triple1)] The cat is not big.[(triple2)] The cat needs the dog.[(triple3)] The cat needs the lion.[(triple4)] The cat sees the rabbit.[(triple5)] The dog eats the cat.[(triple6)] The dog is big.[(triple7)] The dog is red.[(triple8)] The lion does not eat the cat.[(triple9)] The rabbit sees the lion.[(triple10)] @1: The dog is not round.[(((triple6) -> rule2))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cat is not big.
("cat" "is" "big" "-")
triple2
The cat needs the dog.
("cat" "needs" "dog" "+")
triple3
The cat needs the lion.
("cat" "needs" "lion" "+")
triple4
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple5
The dog eats the cat.
("dog" "eats" "cat" "+")
triple6
The dog is big.
("dog" "is" "big" "+")
triple7
The dog is red.
("dog" "is" "red" "+")
triple8
The lion does not eat the cat.
("lion" "eats" "cat" "-")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The dog is not round.
("dog" "is" "round" "-")
((triple6) -> (rule2 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1