The dog does not chase the mouse. The dog chases the squirrel. The lion chases the dog. The lion is round. The mouse is not big. The squirrel chases the mouse. The squirrel needs the dog. If something chases the mouse and the mouse chases the dog then it likes the lion. If something chases the mouse then it is kind. If something chases the dog then it is young. If the mouse needs the squirrel and the squirrel chases the lion then the lion does not like the mouse. If something chases the mouse and the mouse does not need the squirrel then the mouse is big. If the lion is young then the lion chases the mouse. If the squirrel is big then the squirrel needs the dog. If something needs the squirrel and the squirrel likes the lion then the squirrel likes the mouse.
The dog does not chase the mouse.
("dog" "chases" "mouse" "-")
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is round.
("lion" "is" "round" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
If something chases the mouse and the mouse chases the dog then it likes the lion.
((("something" "chases" "mouse" "+") ("mouse" "chases" "dog" "+")) -> ("something" "likes" "lion" "+"))
If something chases the mouse then it is kind.
((("something" "chases" "mouse" "+")) -> ("something" "is" "kind" "+"))
If something chases the dog then it is young.
((("something" "chases" "dog" "+")) -> ("something" "is" "young" "+"))
If the mouse needs the squirrel and the squirrel chases the lion then the lion does not like the mouse.
((("mouse" "needs" "squirrel" "+") ("squirrel" "chases" "lion" "+")) -> ("lion" "likes" "mouse" "-"))
If something chases the mouse and the mouse does not need the squirrel then the mouse is big.
((("something" "chases" "mouse" "+") ("mouse" "needs" "squirrel" "~")) -> ("mouse" "is" "big" "+"))
If the lion is young then the lion chases the mouse.
((("lion" "is" "young" "+")) -> ("lion" "chases" "mouse" "+"))
If the squirrel is big then the squirrel needs the dog.
((("squirrel" "is" "big" "+")) -> ("squirrel" "needs" "dog" "+"))
If something needs the squirrel and the squirrel likes the lion then the squirrel likes the mouse.
((("something" "needs" "squirrel" "+") ("squirrel" "likes" "lion" "+")) -> ("squirrel" "likes" "mouse" "+"))
The mouse is not big.
True
1
proof
[(triple5)]
("mouse" "is" "big" "-")
triple5
The dog does not chase the squirrel.
False
1
inv-proof
[(triple2)]
("dog" "chases" "squirrel" "-")
triple2
The lion is young.
True
2
proof
[(((triple3) -> rule3))]
("lion" "is" "young" "+")
((triple3) -> (rule3 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not young.
False
2
inv-proof
[(((triple3) -> rule3))]
("lion" "is" "young" "-")
((triple3) -> (rule3 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion chases the mouse.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("lion" "chases" "mouse" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion does not chase the mouse.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("lion" "chases" "mouse" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is kind.
True
4
proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule2))]
("lion" "is" "kind" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is not kind.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule2))]
("lion" "is" "kind" "-")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The dog does not like the lion.
Unknown
inv-rconc
[@1: The dog likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "lion" "-")
The lion likes the lion.
Unknown
rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "lion" "+")
The mouse is not young.
Unknown
inv-rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "young" "-")
The squirrel likes the lion.
Unknown
rconc
[@1: The squirrel likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "likes" "lion" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The dog chases the squirrel.[(triple2)] The dog does not chase the mouse.[(triple1)] The lion chases the dog.[(triple3)] The lion is round.[(triple4)] The mouse is not big.[(triple5)] The squirrel chases the mouse.[(triple6)] The squirrel needs the dog.[(triple7)] @1: The lion is young.[(((triple3) -> rule3))] The squirrel is kind.[(((triple6) -> rule2))] @2: The lion chases the mouse.[(((((triple3) -> rule3)) -> rule6))] @3: The lion is kind.[(((((((triple3) -> rule3)) -> rule6)) -> rule2))]
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple2
The dog does not chase the mouse.
("dog" "chases" "mouse" "-")
triple1
The lion chases the dog.
("lion" "chases" "dog" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The mouse is not big.
("mouse" "is" "big" "-")
triple5
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple6
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple7
The lion is young.
("lion" "is" "young" "+")
((triple3) -> (rule3 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple6) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3