The lion chases the mouse. The lion is big. The lion sees the mouse. The mouse chases the lion. The mouse is rough. The mouse is round. The mouse sees the lion. If something chases the mouse and it is rough then it is red. If the lion eats the mouse and the mouse chases the lion then the mouse is big. If something eats the lion and the lion is round then the lion is big. If the lion is big and the lion sees the mouse then the mouse eats the lion. If something is big then it chases the mouse. If something sees the mouse and the mouse chases the lion then the lion eats the mouse.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is big.
("lion" "is" "big" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something chases the mouse and it is rough then it is red.
((("something" "chases" "mouse" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If the lion eats the mouse and the mouse chases the lion then the mouse is big.
((("lion" "eats" "mouse" "+") ("mouse" "chases" "lion" "+")) -> ("mouse" "is" "big" "+"))
If something eats the lion and the lion is round then the lion is big.
((("something" "eats" "lion" "+") ("lion" "is" "round" "+")) -> ("lion" "is" "big" "+"))
If the lion is big and the lion sees the mouse then the mouse eats the lion.
((("lion" "is" "big" "+") ("lion" "sees" "mouse" "+")) -> ("mouse" "eats" "lion" "+"))
If something is big then it chases the mouse.
((("something" "is" "big" "+")) -> ("something" "chases" "mouse" "+"))
If something sees the mouse and the mouse chases the lion then the lion eats the mouse.
((("something" "sees" "mouse" "+") ("mouse" "chases" "lion" "+")) -> ("lion" "eats" "mouse" "+"))
The mouse chases the lion.
True
1
proof
[(triple4)]
("mouse" "chases" "lion" "+")
triple4
The mouse does not see the lion.
False
1
inv-proof
[(triple7)]
("mouse" "sees" "lion" "-")
triple7
The mouse eats the lion.
True
3
proof
[(((triple2 triple3) -> rule4))]
("mouse" "eats" "lion" "+")
((triple2 triple3) -> (rule4 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse does not eat the lion.
False
3
inv-proof
[(((triple2 triple3) -> rule4))]
("mouse" "eats" "lion" "-")
((triple2 triple3) -> (rule4 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse is big.
True
5
proof
[(((((triple3 triple4) -> rule6) triple4) -> rule2))]
("mouse" "is" "big" "+")
((((triple3 triple4) -> (rule6 % int2)) triple4) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The mouse is not big.
False
5
inv-proof
[(((((triple3 triple4) -> rule6) triple4) -> rule2))]
("mouse" "is" "big" "-")
((((triple3 triple4) -> (rule6 % int2)) triple4) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The mouse chases the mouse.
True
6
proof
[(((((((triple3 triple4) -> rule6) triple4) -> rule2)) -> rule5))]
("mouse" "chases" "mouse" "+")
((((((triple3 triple4) -> (rule6 % int3)) triple4) -> (rule2 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int3
The mouse does not chase the mouse.
False
6
inv-proof
[(((((((triple3 triple4) -> rule6) triple4) -> rule2)) -> rule5))]
("mouse" "chases" "mouse" "-")
((((((triple3 triple4) -> (rule6 % int3)) triple4) -> (rule2 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int3
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "red" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "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 nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The lion chases the mouse.[(triple1 OR ((triple2) -> rule5))] The lion is big.[(triple2)] The lion sees the mouse.[(triple3)] The mouse chases the lion.[(triple4)] The mouse is rough.[(triple5)] The mouse is round.[(triple6)] The mouse sees the lion.[(triple7)] @1: The lion eats the mouse.[(((triple3 triple4) -> rule6))] The mouse eats the lion.[(((triple2 triple3) -> rule4))] @2: The mouse is big.[(((((triple3 triple4) -> rule6) triple4) -> rule2))] @3: The mouse chases the mouse.[(((((((triple3 triple4) -> rule6) triple4) -> rule2)) -> rule5))] @4: The mouse is red.[(((((((((triple3 triple4) -> rule6) triple4) -> rule2)) -> rule5) triple5) -> rule1))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
((triple2) -> (rule5 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple3
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse is round.
("mouse" "is" "round" "+")
triple6
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple7
The lion eats the mouse.
("lion" "eats" "mouse" "+")
((triple3 triple4) -> (rule6 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
((triple2 triple3) -> (rule4 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((((triple3 triple4) -> (rule6 % int2)) triple4) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((triple3 triple4) -> (rule6 % int3)) triple4) -> (rule2 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
((((((((triple3 triple4) -> (rule6 % int4)) triple4) -> (rule2 % int3))) -> (rule5 % int2)) triple5) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int4