The mouse is blue. The mouse is cold. The mouse is green. The mouse is red. The mouse likes the rabbit. The mouse needs the rabbit. The mouse visits the rabbit. The rabbit is green. The rabbit likes the mouse. The rabbit needs the mouse. If something is green and it needs the mouse then it is nice. If something is red then it likes the rabbit. If something visits the rabbit and it is nice then it needs the rabbit. If something visits the mouse and it needs the rabbit then it needs the mouse. If something needs the rabbit then the rabbit visits the mouse. If something likes the rabbit and the rabbit likes the mouse then it visits the mouse.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If something is green and it needs the mouse then it is nice.
((("something" "is" "green" "+") ("something" "needs" "mouse" "+")) -> ("something" "is" "nice" "+"))
If something is red then it likes the rabbit.
((("something" "is" "red" "+")) -> ("something" "likes" "rabbit" "+"))
If something visits the rabbit and it is nice then it needs the rabbit.
((("something" "visits" "rabbit" "+") ("something" "is" "nice" "+")) -> ("something" "needs" "rabbit" "+"))
If something visits the mouse and it needs the rabbit then it needs the mouse.
((("something" "visits" "mouse" "+") ("something" "needs" "rabbit" "+")) -> ("something" "needs" "mouse" "+"))
If something needs the rabbit then the rabbit visits the mouse.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "visits" "mouse" "+"))
If something likes the rabbit and the rabbit likes the mouse then it visits the mouse.
((("something" "likes" "rabbit" "+") ("rabbit" "likes" "mouse" "+")) -> ("something" "visits" "mouse" "+"))
The mouse likes the rabbit.
True
1
proof
[(triple5 OR ((triple4) -> rule2))]
("mouse" "likes" "rabbit" "+")
triple5
((triple4) -> (rule2 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The rabbit is not green.
False
1
inv-proof
[(triple8)]
("rabbit" "is" "green" "-")
triple8
The mouse visits the mouse.
True
3
proof
[(((triple5 triple9) -> rule6) OR ((((triple4) -> rule2) triple9) -> rule6))]
("mouse" "visits" "mouse" "+")
((triple5 triple9) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
((((triple4) -> (rule2 % int2)) triple9) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The rabbit does not visit the mouse.
False
2
inv-proof
[(((triple6) -> rule5))]
("rabbit" "visits" "mouse" "-")
((triple6) -> (rule5 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The mouse needs the mouse.
True
5
proof
[(((((triple5 triple9) -> rule6) triple6) -> rule4) OR ((((((triple4) -> rule2) triple9) -> rule6) triple6) -> rule4))]
("mouse" "needs" "mouse" "+")
((((triple5 triple9) -> (rule6 % int2)) triple6) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
((((((triple4) -> (rule2 % int3)) triple9) -> (rule6 % int2)) triple6) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The mouse does not need the mouse.
False
5
inv-proof
[(((((triple5 triple9) -> rule6) triple6) -> rule4) OR ((((((triple4) -> rule2) triple9) -> rule6) triple6) -> rule4))]
("mouse" "needs" "mouse" "-")
((((triple5 triple9) -> (rule6 % int2)) triple6) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
((((((triple4) -> (rule2 % int3)) triple9) -> (rule6 % int2)) triple6) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The mouse is nice.
True
7
proof
[(((triple3 ((((triple5 triple9) -> rule6) triple6) -> rule4)) -> rule1) OR ((triple3 ((((((triple4) -> rule2) triple9) -> rule6) triple6) -> rule4)) -> rule1))]
("mouse" "is" "nice" "+")
((triple3 ((((triple5 triple9) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
((triple3 ((((((triple4) -> (rule2 % int4)) triple9) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The mouse is not nice.
False
7
inv-proof
[(((triple3 ((((triple5 triple9) -> rule6) triple6) -> rule4)) -> rule1) OR ((triple3 ((((((triple4) -> rule2) triple9) -> rule6) triple6) -> rule4)) -> rule1))]
("mouse" "is" "nice" "-")
((triple3 ((((triple5 triple9) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
((triple3 ((((((triple4) -> (rule2 % int4)) triple9) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The mouse is blue.[(triple1)] The mouse is cold.[(triple2)] The mouse is green.[(triple3)] The mouse is red.[(triple4)] The mouse likes the rabbit.[(triple5 OR ((triple4) -> rule2))] The mouse needs the rabbit.[(triple6)] The mouse visits the rabbit.[(triple7)] The rabbit is green.[(triple8)] The rabbit likes the mouse.[(triple9)] The rabbit needs the mouse.[(triple10)] @1: The mouse visits the mouse.[(((triple5 triple9) -> rule6) OR ((((triple4) -> rule2) triple9) -> rule6))] The rabbit is nice.[(((triple8 triple10) -> rule1))] The rabbit visits the mouse.[(((triple6) -> rule5))] @2: The mouse needs the mouse.[(((((triple5 triple9) -> rule6) triple6) -> rule4) OR ((((((triple4) -> rule2) triple9) -> rule6) triple6) -> rule4))] @3: The mouse is nice.[(((triple3 ((((triple5 triple9) -> rule6) triple6) -> rule4)) -> rule1) OR ((triple3 ((((((triple4) -> rule2) triple9) -> rule6) triple6) -> rule4)) -> rule1))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse is red.
("mouse" "is" "red" "+")
triple4
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple5
((triple4) -> (rule2 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple6
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple7
The rabbit is green.
("rabbit" "is" "green" "+")
triple8
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple9
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple10
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple5 triple9) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
((((triple4) -> (rule2 % int2)) triple9) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple8 triple10) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
((triple6) -> (rule5 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple5 triple9) -> (rule6 % int2)) triple6) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
((((((triple4) -> (rule2 % int3)) triple9) -> (rule6 % int2)) triple6) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
((triple3 ((((triple5 triple9) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
((triple3 ((((((triple4) -> (rule2 % int4)) triple9) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4