The mouse is blue. The mouse is cold. The mouse is green. The mouse is nice. The mouse is round. The mouse needs the rabbit. The mouse sees the rabbit. The mouse visits the rabbit. The rabbit is blue. The rabbit is cold. The rabbit is green. The rabbit is nice. The rabbit needs the mouse. The rabbit sees the mouse. The rabbit visits the mouse. If something sees the rabbit and the rabbit is round then it needs the rabbit. If something is cold then it is blue. If the rabbit visits the mouse and the mouse visits the rabbit then the rabbit sees the mouse. If something is blue and it visits the mouse then the mouse needs the rabbit. If something sees the rabbit then it needs the rabbit. If something is green and it visits the rabbit then the rabbit visits the mouse. If the mouse visits the rabbit and the rabbit needs the mouse then the mouse is blue. If something visits the mouse then it sees the rabbit.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something sees the rabbit and the rabbit is round then it needs the rabbit.
((("something" "sees" "rabbit" "+") ("rabbit" "is" "round" "+")) -> ("something" "needs" "rabbit" "+"))
If something is cold then it is blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If the rabbit visits the mouse and the mouse visits the rabbit then the rabbit sees the mouse.
((("rabbit" "visits" "mouse" "+") ("mouse" "visits" "rabbit" "+")) -> ("rabbit" "sees" "mouse" "+"))
If something is blue and it visits the mouse then the mouse needs the rabbit.
((("something" "is" "blue" "+") ("something" "visits" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
If something sees the rabbit then it needs the rabbit.
((("something" "sees" "rabbit" "+")) -> ("something" "needs" "rabbit" "+"))
If something is green and it visits the rabbit then the rabbit visits the mouse.
((("something" "is" "green" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "mouse" "+"))
If the mouse visits the rabbit and the rabbit needs the mouse then the mouse is blue.
((("mouse" "visits" "rabbit" "+") ("rabbit" "needs" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If something visits the mouse then it sees the rabbit.
((("something" "visits" "mouse" "+")) -> ("something" "sees" "rabbit" "+"))
The mouse needs the rabbit.
True
1
proof
[(triple6 OR ((triple7) -> rule5) OR ((triple9 triple15) -> rule4) OR ((triple9 ((triple3 triple8) -> rule6)) -> rule4) OR ((((triple10) -> rule2) triple15) -> rule4) OR ((((triple10) -> rule2) ((triple3 triple8) -> rule6)) -> rule4))]
("mouse" "needs" "rabbit" "+")
triple6
((triple7) -> (rule5 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
((triple9 triple15) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
((triple9 ((triple3 triple8) -> (rule6 % int2))) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
((((triple10) -> (rule2 % int2)) triple15) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((((triple10) -> (rule2 % int3)) ((triple3 triple8) -> (rule6 % int2))) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The mouse is not blue.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule2) OR ((triple8 triple13) -> rule7))]
("mouse" "is" "blue" "-")
triple1
((triple2) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple8 triple13) -> (rule7 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The rabbit sees the rabbit.
True
2
proof
[(((triple15) -> rule8) OR ((((triple3 triple8) -> rule6)) -> rule8))]
("rabbit" "sees" "rabbit" "+")
((triple15) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
((((triple3 triple8) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The rabbit does not see the rabbit.
False
2
inv-proof
[(((triple15) -> rule8) OR ((((triple3 triple8) -> rule6)) -> rule8))]
("rabbit" "sees" "rabbit" "-")
((triple15) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
((((triple3 triple8) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The rabbit needs the rabbit.
True
3
proof
[(((((triple15) -> rule8)) -> rule5) OR ((((((triple3 triple8) -> rule6)) -> rule8)) -> rule5))]
("rabbit" "needs" "rabbit" "+")
((((triple15) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
((((((triple3 triple8) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int3
The rabbit does not need the rabbit.
False
3
inv-proof
[(((((triple15) -> rule8)) -> rule5) OR ((((((triple3 triple8) -> rule6)) -> rule8)) -> rule5))]
("rabbit" "needs" "rabbit" "-")
((((triple15) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
((((((triple3 triple8) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int3
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 mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The mouse is blue.[(triple1 OR ((triple2) -> rule2) OR ((triple8 triple13) -> rule7))] The mouse is cold.[(triple2)] The mouse is green.[(triple3)] The mouse is nice.[(triple4)] The mouse is round.[(triple5)] The mouse needs the rabbit.[(triple6 OR ((triple7) -> rule5) OR ((triple9 triple15) -> rule4) OR ((triple9 ((triple3 triple8) -> rule6)) -> rule4) OR ((((triple10) -> rule2) triple15) -> rule4) OR ((((triple10) -> rule2) ((triple3 triple8) -> rule6)) -> rule4))] The mouse sees the rabbit.[(triple7)] The mouse visits the rabbit.[(triple8)] The rabbit is blue.[(triple9 OR ((triple10) -> rule2))] The rabbit is cold.[(triple10)] The rabbit is green.[(triple11)] The rabbit is nice.[(triple12)] The rabbit needs the mouse.[(triple13)] The rabbit sees the mouse.[(triple14 OR ((triple15 triple8) -> rule3) OR ((((triple3 triple8) -> rule6) triple8) -> rule3))] The rabbit visits the mouse.[(triple15 OR ((triple3 triple8) -> rule6))] @1: The rabbit sees the rabbit.[(((triple15) -> rule8) OR ((((triple3 triple8) -> rule6)) -> rule8))] @2: The rabbit needs the rabbit.[(((((triple15) -> rule8)) -> rule5) OR ((((((triple3 triple8) -> rule6)) -> rule8)) -> rule5))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
((triple2) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple8 triple13) -> (rule7 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse is round.
("mouse" "is" "round" "+")
triple5
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple6
((triple7) -> (rule5 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
((triple9 triple15) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
((triple9 ((triple3 triple8) -> (rule6 % int2))) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
((((triple10) -> (rule2 % int2)) triple15) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((((triple10) -> (rule2 % int3)) ((triple3 triple8) -> (rule6 % int2))) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple7
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
((triple10) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple10
The rabbit is green.
("rabbit" "is" "green" "+")
triple11
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple12
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple13
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple14
((triple15 triple8) -> (rule3 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
((((triple3 triple8) -> (rule6 % int2)) triple8) -> (rule3 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple15
((triple3 triple8) -> (rule6 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple15) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
((((triple3 triple8) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((triple15) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
((((((triple3 triple8) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int3