The bear chases the rabbit. The bear chases the squirrel. The bear is rough. The bear sees the rabbit. The bear sees the squirrel. The bear visits the rabbit. The rabbit chases the bear. The rabbit visits the bear. The squirrel chases the bear. The squirrel is not young. The squirrel sees the bear. The squirrel sees the rabbit. If something visits the rabbit and it sees the bear then it is rough. If the squirrel sees the rabbit then the squirrel visits the rabbit. If something sees the squirrel then the squirrel visits the rabbit. If the rabbit is cold then the rabbit does not chase the bear. If something sees the bear and it is not cold then the bear is not young. If something sees the squirrel and the squirrel is rough then it is young. If something is blue then it chases the bear. If something sees the squirrel and the squirrel is cold then the squirrel is young.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel is not young.
("squirrel" "is" "young" "-")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If something visits the rabbit and it sees the bear then it is rough.
((("something" "visits" "rabbit" "+") ("something" "sees" "bear" "+")) -> ("something" "is" "rough" "+"))
If the squirrel sees the rabbit then the squirrel visits the rabbit.
((("squirrel" "sees" "rabbit" "+")) -> ("squirrel" "visits" "rabbit" "+"))
If something sees the squirrel then the squirrel visits the rabbit.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "visits" "rabbit" "+"))
If the rabbit is cold then the rabbit does not chase the bear.
((("rabbit" "is" "cold" "+")) -> ("rabbit" "chases" "bear" "-"))
If something sees the bear and it is not cold then the bear is not young.
((("something" "sees" "bear" "+") ("something" "is" "cold" "~")) -> ("bear" "is" "young" "-"))
If something sees the squirrel and the squirrel is rough then it is young.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is blue then it chases the bear.
((("something" "is" "blue" "+")) -> ("something" "chases" "bear" "+"))
If something sees the squirrel and the squirrel is cold then the squirrel is young.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "cold" "+")) -> ("squirrel" "is" "young" "+"))
The squirrel is not young.
True
1
proof
[(triple10)]
("squirrel" "is" "young" "-")
triple10
The squirrel does not see the rabbit.
False
1
inv-proof
[(triple12)]
("squirrel" "sees" "rabbit" "-")
triple12
The squirrel visits the rabbit.
True
2
proof
[(((triple12) -> rule2) OR ((triple5) -> rule3))]
("squirrel" "visits" "rabbit" "+")
((triple12) -> (rule2 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
((triple5) -> (rule3 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The squirrel does not visit the rabbit.
False
2
inv-proof
[(((triple12) -> rule2) OR ((triple5) -> rule3))]
("squirrel" "visits" "rabbit" "-")
((triple12) -> (rule2 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
((triple5) -> (rule3 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The squirrel is rough.
True
4
proof
[(((((triple12) -> rule2) triple11) -> rule1) OR ((((triple5) -> rule3) triple11) -> rule1))]
("squirrel" "is" "rough" "+")
((((triple12) -> (rule2 % int2)) triple11) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
((((triple5) -> (rule3 % int2)) triple11) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The squirrel is not rough.
False
4
inv-proof
[(((((triple12) -> rule2) triple11) -> rule1) OR ((((triple5) -> rule3) triple11) -> rule1))]
("squirrel" "is" "rough" "-")
((((triple12) -> (rule2 % int2)) triple11) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
((((triple5) -> (rule3 % int2)) triple11) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The bear is young.
True
6
proof
[(((triple5 ((((triple12) -> rule2) triple11) -> rule1)) -> rule6) OR ((triple5 ((((triple5) -> rule3) triple11) -> rule1)) -> rule6))]
("bear" "is" "young" "+")
((triple5 ((((triple12) -> (rule2 % int3)) triple11) -> (rule1 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3
((triple5 ((((triple5) -> (rule3 % int3)) triple11) -> (rule1 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3
The bear is not young.
False
6
inv-proof
[(((triple5 ((((triple12) -> rule2) triple11) -> rule1)) -> rule6) OR ((triple5 ((((triple5) -> rule3) triple11) -> rule1)) -> rule6))]
("bear" "is" "young" "-")
((triple5 ((((triple12) -> (rule2 % int3)) triple11) -> (rule1 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3
((triple5 ((((triple5) -> (rule3 % int3)) triple11) -> (rule1 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "chases" "bear" "-")
The rabbit is rough.
Unknown
rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "rough" "+")
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "young" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
The squirrel does not visit the bear.
Unknown
inv-random
[@0: The squirrel visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bear" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit sees the bear.
Unknown
random
[@0: The rabbit sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bear" "+")
@0: The bear chases the rabbit.[(triple1)] The bear chases the squirrel.[(triple2)] The bear is rough.[(triple3)] The bear sees the rabbit.[(triple4)] The bear sees the squirrel.[(triple5)] The bear visits the rabbit.[(triple6)] The rabbit chases the bear.[(triple7)] The rabbit visits the bear.[(triple8)] The squirrel chases the bear.[(triple9)] The squirrel is not young.[(triple10)] The squirrel sees the bear.[(triple11)] The squirrel sees the rabbit.[(triple12)] @1: The squirrel visits the rabbit.[(((triple12) -> rule2) OR ((triple5) -> rule3))] @2: The squirrel is rough.[(((((triple12) -> rule2) triple11) -> rule1) OR ((((triple5) -> rule3) triple11) -> rule1))] @3: The bear is young.[(((triple5 ((((triple12) -> rule2) triple11) -> rule1)) -> rule6) OR ((triple5 ((((triple5) -> rule3) triple11) -> rule1)) -> rule6))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple4
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple5
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple6
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple7
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple8
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple9
The squirrel is not young.
("squirrel" "is" "young" "-")
triple10
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple11
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple12
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
((triple12) -> (rule2 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
((triple5) -> (rule3 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((triple12) -> (rule2 % int2)) triple11) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
((((triple5) -> (rule3 % int2)) triple11) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The bear is young.
("bear" "is" "young" "+")
((triple5 ((((triple12) -> (rule2 % int3)) triple11) -> (rule1 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3
((triple5 ((((triple5) -> (rule3 % int3)) triple11) -> (rule1 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int3