The cat likes the mouse. The dog eats the cat. The dog is blue. The dog is young. The mouse eats the squirrel. The mouse is not young. The mouse likes the cat. The mouse likes the squirrel. The squirrel likes the mouse. The squirrel visits the cat. All big things are not young. If something eats the mouse and it is young then the mouse likes the dog. If something visits the cat then it eats the cat. If something eats the cat and it visits the cat then it is big. If the cat visits the dog and the cat eats the dog then the cat is rough. If something eats the mouse then the mouse is big.
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is young.
("dog" "is" "young" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
All big things are not young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "-"))
If something eats the mouse and it is young then the mouse likes the dog.
((("something" "eats" "mouse" "+") ("something" "is" "young" "+")) -> ("mouse" "likes" "dog" "+"))
If something visits the cat then it eats the cat.
((("something" "visits" "cat" "+")) -> ("something" "eats" "cat" "+"))
If something eats the cat and it visits the cat then it is big.
((("something" "eats" "cat" "+") ("something" "visits" "cat" "+")) -> ("something" "is" "big" "+"))
If the cat visits the dog and the cat eats the dog then the cat is rough.
((("cat" "visits" "dog" "+") ("cat" "eats" "dog" "+")) -> ("cat" "is" "rough" "+"))
If something eats the mouse then the mouse is big.
((("something" "eats" "mouse" "+")) -> ("mouse" "is" "big" "+"))
The squirrel likes the mouse.
True
1
proof
[(triple9)]
("squirrel" "likes" "mouse" "+")
triple9
The dog does not eat the cat.
False
1
inv-proof
[(triple2)]
("dog" "eats" "cat" "-")
triple2
The squirrel eats the cat.
True
2
proof
[(((triple10) -> rule3))]
("squirrel" "eats" "cat" "+")
((triple10) -> (rule3 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel does not eat the cat.
False
2
inv-proof
[(((triple10) -> rule3))]
("squirrel" "eats" "cat" "-")
((triple10) -> (rule3 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel is big.
True
4
proof
[(((((triple10) -> rule3) triple10) -> rule4))]
("squirrel" "is" "big" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel is not big.
False
4
inv-proof
[(((((triple10) -> rule3) triple10) -> rule4))]
("squirrel" "is" "big" "-")
((((triple10) -> (rule3 % int2)) triple10) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel is not young.
True
5
proof
[(((((((triple10) -> rule3) triple10) -> rule4)) -> rule1))]
("squirrel" "is" "young" "-")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int3
The squirrel is young.
False
5
inv-proof
[(((((((triple10) -> rule3) triple10) -> rule4)) -> rule1))]
("squirrel" "is" "young" "+")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int3
The mouse does not eat the cat.
Unknown
inv-rconc
[@1: The mouse eats the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "eats" "cat" "-")
The mouse likes the dog.
Unknown
rconc
[@1: The mouse likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "dog" "+")
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "big" "-")
The cat is big.
Unknown
rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "big" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The dog visits the cat.
Unknown
random
[@0: The dog visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "cat" "+")
The dog does not visit the mouse.
Unknown
inv-random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The cat likes the mouse.[(triple1)] The dog eats the cat.[(triple2)] The dog is blue.[(triple3)] The dog is young.[(triple4)] The mouse eats the squirrel.[(triple5)] The mouse is not young.[(triple6)] The mouse likes the cat.[(triple7)] The mouse likes the squirrel.[(triple8)] The squirrel likes the mouse.[(triple9)] The squirrel visits the cat.[(triple10)] @1: The squirrel eats the cat.[(((triple10) -> rule3))] @2: The squirrel is big.[(((((triple10) -> rule3) triple10) -> rule4))] @3: The squirrel is not young.[(((((((triple10) -> rule3) triple10) -> rule4)) -> rule1))]
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple1
The dog eats the cat.
("dog" "eats" "cat" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple5
The mouse is not young.
("mouse" "is" "young" "-")
triple6
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple7
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple8
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple9
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple10
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
((triple10) -> (rule3 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel is not young.
("squirrel" "is" "young" "-")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int3