The lion eats the mouse. The lion is cold. The lion is kind. The lion is red. The lion likes the mouse. The lion does not need the mouse. The mouse eats the lion. The mouse is kind. The mouse is nice. The mouse is red. The mouse likes the lion. The mouse needs the lion. If the mouse needs the lion and the mouse is red then the lion likes the mouse. If someone likes the mouse then the mouse is red. If someone eats the mouse then they are blue. If someone likes the mouse then they are blue. If someone eats the lion and the lion is blue then the lion is nice. If someone likes the mouse and the mouse needs the lion then the mouse eats the lion.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If the mouse needs the lion and the mouse is red then the lion likes the mouse.
((("mouse" "needs" "lion" "+") ("mouse" "is" "red" "+")) -> ("lion" "likes" "mouse" "+"))
If someone likes the mouse then the mouse is red.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "red" "+"))
If someone eats the mouse then they are blue.
((("someone" "eats" "mouse" "+")) -> ("someone" "is" "blue" "+"))
If someone likes the mouse then they are blue.
((("someone" "likes" "mouse" "+")) -> ("someone" "is" "blue" "+"))
If someone eats the lion and the lion is blue then the lion is nice.
((("someone" "eats" "lion" "+") ("lion" "is" "blue" "+")) -> ("lion" "is" "nice" "+"))
If someone likes the mouse and the mouse needs the lion then the mouse eats the lion.
((("someone" "likes" "mouse" "+") ("mouse" "needs" "lion" "+")) -> ("mouse" "eats" "lion" "+"))
The mouse is kind.
True
1
proof
[(triple8)]
("mouse" "is" "kind" "+")
triple8
The mouse is not kind.
False
1
inv-proof
[(triple8)]
("mouse" "is" "kind" "-")
triple8
The lion is blue.
True
2
proof
[(((triple1) -> rule3) OR ((triple5) -> rule4) OR ((((triple12 triple10) -> rule1)) -> rule4))]
("lion" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((triple5) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((((triple12 triple10) -> (rule1 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The lion is not blue.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple5) -> rule4) OR ((((triple12 triple10) -> rule1)) -> rule4))]
("lion" "is" "blue" "-")
((triple1) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((triple5) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((((triple12 triple10) -> (rule1 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The lion is nice.
True
4
proof
[(((triple7 ((triple1) -> rule3)) -> rule5) OR ((triple7 ((triple5) -> rule4)) -> rule5) OR ((((triple5 triple12) -> rule6) ((triple1) -> rule3)) -> rule5) OR ((((triple5 triple12) -> rule6) ((triple5) -> rule4)) -> rule5) OR ((triple7 ((((triple12 triple10) -> rule1)) -> rule4)) -> rule5) OR ((((triple5 triple12) -> rule6) ((((triple12 triple10) -> rule1)) -> rule4)) -> rule5) OR ((((((triple12 triple10) -> rule1) triple12) -> rule6) ((triple1) -> rule3)) -> rule5) OR ((((((triple12 triple10) -> rule1) triple12) -> rule6) ((triple5) -> rule4)) -> rule5) OR ((((((triple12 triple10) -> rule1) triple12) -> rule6) ((((triple12 triple10) -> rule1)) -> rule4)) -> rule5))]
("lion" "is" "nice" "+")
((triple7 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((triple7 ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple5 triple12) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
((((triple5 triple12) -> (rule6 % int3)) ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
((triple7 ((((triple12 triple10) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
((((triple5 triple12) -> (rule6 % int4)) ((((triple12 triple10) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int4
((((((triple12 triple10) -> (rule1 % int4)) triple12) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
((((((triple12 triple10) -> (rule1 % int4)) triple12) -> (rule6 % int3)) ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
((((((triple12 triple10) -> (rule1 % int4)) triple12) -> (rule6 % int3)) ((((triple12 triple10) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
The lion is not nice.
False
4
inv-proof
[(((triple7 ((triple1) -> rule3)) -> rule5) OR ((triple7 ((triple5) -> rule4)) -> rule5) OR ((((triple5 triple12) -> rule6) ((triple1) -> rule3)) -> rule5) OR ((((triple5 triple12) -> rule6) ((triple5) -> rule4)) -> rule5) OR ((triple7 ((((triple12 triple10) -> rule1)) -> rule4)) -> rule5) OR ((((triple5 triple12) -> rule6) ((((triple12 triple10) -> rule1)) -> rule4)) -> rule5) OR ((((((triple12 triple10) -> rule1) triple12) -> rule6) ((triple1) -> rule3)) -> rule5) OR ((((((triple12 triple10) -> rule1) triple12) -> rule6) ((triple5) -> rule4)) -> rule5) OR ((((((triple12 triple10) -> rule1) triple12) -> rule6) ((((triple12 triple10) -> rule1)) -> rule4)) -> rule5))]
("lion" "is" "nice" "-")
((triple7 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((triple7 ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple5 triple12) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
((((triple5 triple12) -> (rule6 % int3)) ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
((triple7 ((((triple12 triple10) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
((((triple5 triple12) -> (rule6 % int4)) ((((triple12 triple10) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int4
((((((triple12 triple10) -> (rule1 % int4)) triple12) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
((((((triple12 triple10) -> (rule1 % int4)) triple12) -> (rule6 % int3)) ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
((((((triple12 triple10) -> (rule1 % int4)) triple12) -> (rule6 % int3)) ((((triple12 triple10) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "blue" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
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 mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The lion does not need the mouse.[(triple6)] The lion eats the mouse.[(triple1)] The lion is cold.[(triple2)] The lion is kind.[(triple3)] The lion is red.[(triple4)] The lion likes the mouse.[(triple5 OR ((triple12 triple10) -> rule1))] The mouse eats the lion.[(triple7 OR ((triple5 triple12) -> rule6) OR ((((triple12 triple10) -> rule1) triple12) -> rule6))] The mouse is kind.[(triple8)] The mouse is nice.[(triple9)] The mouse is red.[(triple10 OR ((triple5) -> rule2))] The mouse likes the lion.[(triple11)] The mouse needs the lion.[(triple12)] @1: The lion is blue.[(((triple1) -> rule3) OR ((triple5) -> rule4) OR ((((triple12 triple10) -> rule1)) -> rule4))] @2: The lion is nice.[(((triple7 ((triple1) -> rule3)) -> rule5) OR ((triple7 ((triple5) -> rule4)) -> rule5) OR ((((triple5 triple12) -> rule6) ((triple1) -> rule3)) -> rule5) OR ((((triple5 triple12) -> rule6) ((triple5) -> rule4)) -> rule5) OR ((triple7 ((((triple12 triple10) -> rule1)) -> rule4)) -> rule5) OR ((((triple5 triple12) -> rule6) ((((triple12 triple10) -> rule1)) -> rule4)) -> rule5) OR ((((((triple12 triple10) -> rule1) triple12) -> rule6) ((triple1) -> rule3)) -> rule5) OR ((((((triple12 triple10) -> rule1) triple12) -> rule6) ((triple5) -> rule4)) -> rule5) OR ((((((triple12 triple10) -> rule1) triple12) -> rule6) ((((triple12 triple10) -> rule1)) -> rule4)) -> rule5))]
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
triple6
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion is red.
("lion" "is" "red" "+")
triple4
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple5
((triple12 triple10) -> (rule1 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple7
((triple5 triple12) -> (rule6 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
((((triple12 triple10) -> (rule1 % int2)) triple12) -> (rule6 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
triple8
The mouse is nice.
("mouse" "is" "nice" "+")
triple9
The mouse is red.
("mouse" "is" "red" "+")
triple10
((triple5) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple11
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple12
The lion is blue.
("lion" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((triple5) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((((triple12 triple10) -> (rule1 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
((triple7 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((triple7 ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple5 triple12) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
((((triple5 triple12) -> (rule6 % int3)) ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
((triple7 ((((triple12 triple10) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
((((triple5 triple12) -> (rule6 % int4)) ((((triple12 triple10) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int4
((((((triple12 triple10) -> (rule1 % int4)) triple12) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
((((((triple12 triple10) -> (rule1 % int4)) triple12) -> (rule6 % int3)) ((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
((((((triple12 triple10) -> (rule1 % int4)) triple12) -> (rule6 % int3)) ((((triple12 triple10) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4