The dog needs the squirrel. The lion eats the dog. The mouse likes the squirrel. The mouse does not need the dog. The squirrel eats the dog. The squirrel eats the mouse. The squirrel does not need the lion. If something likes the lion then the lion eats the mouse. If something eats the mouse and the mouse likes the dog then it is not big. All blue, round things are not big. If the squirrel is nice then the squirrel is big. If something eats the mouse and the mouse likes the squirrel then it likes the lion. If the dog does not like the lion then the lion likes the mouse.
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse does not need the dog.
("mouse" "needs" "dog" "-")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel does not need the lion.
("squirrel" "needs" "lion" "-")
If something likes the lion then the lion eats the mouse.
((("something" "likes" "lion" "+")) -> ("lion" "eats" "mouse" "+"))
If something eats the mouse and the mouse likes the dog then it is not big.
((("something" "eats" "mouse" "+") ("mouse" "likes" "dog" "+")) -> ("something" "is" "big" "-"))
All blue, round things are not big.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "-"))
If the squirrel is nice then the squirrel is big.
((("squirrel" "is" "nice" "+")) -> ("squirrel" "is" "big" "+"))
If something eats the mouse and the mouse likes the squirrel then it likes the lion.
((("something" "eats" "mouse" "+") ("mouse" "likes" "squirrel" "+")) -> ("something" "likes" "lion" "+"))
If the dog does not like the lion then the lion likes the mouse.
((("dog" "likes" "lion" "~")) -> ("lion" "likes" "mouse" "+"))
The squirrel eats the mouse.
True
1
proof
[(triple6)]
("squirrel" "eats" "mouse" "+")
triple6
The mouse needs the dog.
False
1
inv-proof
[(triple4)]
("mouse" "needs" "dog" "+")
triple4
The squirrel likes the lion.
True
3
proof
[(((triple6 triple3) -> rule5))]
("squirrel" "likes" "lion" "+")
((triple6 triple3) -> (rule5 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel does not like the lion.
False
3
inv-proof
[(((triple6 triple3) -> rule5))]
("squirrel" "likes" "lion" "-")
((triple6 triple3) -> (rule5 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The lion eats the mouse.
True
4
proof
[(((((triple6 triple3) -> rule5)) -> rule1))]
("lion" "eats" "mouse" "+")
((((triple6 triple3) -> (rule5 % int2))) -> (rule1 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The lion does not eat the mouse.
False
4
inv-proof
[(((((triple6 triple3) -> rule5)) -> rule1))]
("lion" "eats" "mouse" "-")
((((triple6 triple3) -> (rule5 % int2))) -> (rule1 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The lion likes the lion.
True
6
proof
[(((((((triple6 triple3) -> rule5)) -> rule1) triple3) -> rule5))]
("lion" "likes" "lion" "+")
((((((triple6 triple3) -> (rule5 % int3))) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int3
The lion does not like the lion.
False
6
inv-proof
[(((((((triple6 triple3) -> rule5)) -> rule1) triple3) -> rule5))]
("lion" "likes" "lion" "-")
((((((triple6 triple3) -> (rule5 % int3))) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int3
The lion does not like the mouse.
Unknown
inv-rconc
[@1: The lion likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "likes" "mouse" "-")
The dog likes the lion.
Unknown
rconc
[@1: The dog likes the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "likes" "lion" "+")
The mouse does not like the lion.
Unknown
inv-rconc
[@1: The mouse likes the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "likes" "lion" "-")
The squirrel is big.
Unknown
rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "big" "+")
The squirrel does not like the dog.
Unknown
inv-random
[@0: The squirrel likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "dog" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The squirrel eats the lion.
Unknown
random
[@0: The squirrel eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "lion" "+")
@0: The dog needs the squirrel.[(triple1)] The lion eats the dog.[(triple2)] The mouse does not need the dog.[(triple4)] The mouse likes the squirrel.[(triple3)] The squirrel does not need the lion.[(triple7)] The squirrel eats the dog.[(triple5)] The squirrel eats the mouse.[(triple6)] @1: The squirrel likes the lion.[(((triple6 triple3) -> rule5))] @2: The lion eats the mouse.[(((((triple6 triple3) -> rule5)) -> rule1))] @3: The lion likes the lion.[(((((((triple6 triple3) -> rule5)) -> rule1) triple3) -> rule5))]
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple1
The lion eats the dog.
("lion" "eats" "dog" "+")
triple2
The mouse does not need the dog.
("mouse" "needs" "dog" "-")
triple4
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple3
The squirrel does not need the lion.
("squirrel" "needs" "lion" "-")
triple7
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple5
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple6
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
((triple6 triple3) -> (rule5 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
((((triple6 triple3) -> (rule5 % int2))) -> (rule1 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
((((((triple6 triple3) -> (rule5 % int3))) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int3