The lion chases the mouse. The lion likes the mouse. The mouse chases the lion. The mouse eats the lion. The mouse is big. The mouse is blue. The mouse is cold. The mouse is round. The mouse is young. The mouse likes the lion. If something likes the lion then it chases the mouse. If something chases the mouse then it likes the mouse. If something likes the lion and it likes the mouse then the lion is round.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
If something likes the lion then it chases the mouse.
((("something" "likes" "lion" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the mouse then it likes the mouse.
((("something" "chases" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
If something likes the lion and it likes the mouse then the lion is round.
((("something" "likes" "lion" "+") ("something" "likes" "mouse" "+")) -> ("lion" "is" "round" "+"))
The mouse is young.
True
1
proof
[(triple9)]
("mouse" "is" "young" "+")
triple9
The mouse is not big.
False
1
inv-proof
[(triple5)]
("mouse" "is" "big" "-")
triple5
The mouse chases the mouse.
True
2
proof
[(((triple10) -> rule1))]
("mouse" "chases" "mouse" "+")
((triple10) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
False
2
inv-proof
[(((triple10) -> rule1))]
("mouse" "chases" "mouse" "-")
((triple10) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the mouse.
True
3
proof
[(((((triple10) -> rule1)) -> rule2))]
("mouse" "likes" "mouse" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse does not like the mouse.
False
3
inv-proof
[(((((triple10) -> rule1)) -> rule2))]
("mouse" "likes" "mouse" "-")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
The lion does not eat the mouse.
Unknown
inv-random
[@0: The lion eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "mouse" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The lion chases the mouse.[(triple1)] The lion likes the mouse.[(triple2 OR ((triple1) -> rule2))] The mouse chases the lion.[(triple3)] The mouse eats the lion.[(triple4)] The mouse is big.[(triple5)] The mouse is blue.[(triple6)] The mouse is cold.[(triple7)] The mouse is round.[(triple8)] The mouse is young.[(triple9)] The mouse likes the lion.[(triple10)] @1: The mouse chases the mouse.[(((triple10) -> rule1))] @2: The mouse likes the mouse.[(((((triple10) -> rule1)) -> rule2))] @3: The lion is round.[(((triple10 ((((triple10) -> rule1)) -> rule2)) -> rule3))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple2
((triple1) -> (rule2 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple4
The mouse is big.
("mouse" "is" "big" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The mouse is round.
("mouse" "is" "round" "+")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple9
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple10
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple10) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The lion is round.
("lion" "is" "round" "+")
((triple10 ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3