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