The cat does not eat the lion. The cat eats the mouse. The cat is nice. The cat is round. The cat likes the lion. The cat likes the mouse. The dog is red. The dog is young. The dog likes the cat. The dog needs the lion. The lion is young. The lion does not need the dog. The mouse is rough. The mouse likes the cat. The mouse needs the lion. If the mouse is round then the mouse does not eat the cat. Rough people are round. If someone likes the mouse and they like the cat then the cat needs the lion. If the dog does not eat the mouse then the mouse needs the cat. If someone needs the cat then they eat the dog. If the mouse likes the dog and the dog likes the lion then the lion needs the mouse.
The cat does not eat the lion.
("cat" "eats" "lion" "-")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion is young.
("lion" "is" "young" "+")
The lion does not need the dog.
("lion" "needs" "dog" "-")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If the mouse is round then the mouse does not eat the cat.
((("mouse" "is" "round" "+")) -> ("mouse" "eats" "cat" "-"))
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone likes the mouse and they like the cat then the cat needs the lion.
((("someone" "likes" "mouse" "+") ("someone" "likes" "cat" "+")) -> ("cat" "needs" "lion" "+"))
If the dog does not eat the mouse then the mouse needs the cat.
((("dog" "eats" "mouse" "~")) -> ("mouse" "needs" "cat" "+"))
If someone needs the cat then they eat the dog.
((("someone" "needs" "cat" "+")) -> ("someone" "eats" "dog" "+"))
If the mouse likes the dog and the dog likes the lion then the lion needs the mouse.
((("mouse" "likes" "dog" "+") ("dog" "likes" "lion" "+")) -> ("lion" "needs" "mouse" "+"))
The dog is red.
True
1
proof
[(triple7)]
("dog" "is" "red" "+")
triple7
The cat is not round.
False
1
inv-proof
[(triple4)]
("cat" "is" "round" "-")
triple4
The mouse is round.
True
2
proof
[(((triple13) -> rule2))]
("mouse" "is" "round" "+")
((triple13) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is not round.
False
2
inv-proof
[(((triple13) -> rule2))]
("mouse" "is" "round" "-")
((triple13) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse does not eat the cat.
True
3
proof
[(((((triple13) -> rule2)) -> rule1))]
("mouse" "eats" "cat" "-")
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not eat the cat.
("mouse" "eats" "cat" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse eats the cat.
False
3
inv-proof
[(((((triple13) -> rule2)) -> rule1))]
("mouse" "eats" "cat" "+")
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not eat the cat.
("mouse" "eats" "cat" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "dog" "-")
The lion needs the mouse.
Unknown
rconc
[@1: The lion needs the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "needs" "mouse" "+")
The mouse does not eat the dog.
Unknown
inv-rconc
[@2: The mouse eats the dog.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("mouse" "eats" "dog" "-")
The mouse needs the dog.
Unknown
random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The lion likes the cat.
Unknown
random
[@0: The lion likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cat" "+")
@0: The cat does not eat the lion.[(triple1)] The cat eats the mouse.[(triple2)] The cat is nice.[(triple3)] The cat is round.[(triple4)] The cat likes the lion.[(triple5)] The cat likes the mouse.[(triple6)] The dog is red.[(triple7)] The dog is young.[(triple8)] The dog likes the cat.[(triple9)] The dog needs the lion.[(triple10)] The lion does not need the dog.[(triple12)] The lion is young.[(triple11)] The mouse is rough.[(triple13)] The mouse likes the cat.[(triple14)] The mouse needs the lion.[(triple15)] @1: The mouse is round.[(((triple13) -> rule2))] @2: The mouse does not eat the cat.[(((((triple13) -> rule2)) -> rule1))]
The cat does not eat the lion.
("cat" "eats" "lion" "-")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat likes the lion.
("cat" "likes" "lion" "+")
triple5
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple6
The dog is red.
("dog" "is" "red" "+")
triple7
The dog is young.
("dog" "is" "young" "+")
triple8
The dog likes the cat.
("dog" "likes" "cat" "+")
triple9
The dog needs the lion.
("dog" "needs" "lion" "+")
triple10
The lion does not need the dog.
("lion" "needs" "dog" "-")
triple12
The lion is young.
("lion" "is" "young" "+")
triple11
The mouse is rough.
("mouse" "is" "rough" "+")
triple13
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple14
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple15
The mouse is round.
("mouse" "is" "round" "+")
((triple13) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse does not eat the cat.
("mouse" "eats" "cat" "-")
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not eat the cat.
("mouse" "eats" "cat" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2