The rabbit chases the squirrel. The rabbit is cold. The rabbit is green. The rabbit is not red. The rabbit is young. The rabbit sees the squirrel. The rabbit visits the squirrel. The squirrel does not chase the rabbit. The squirrel is kind. The squirrel is young. The squirrel sees the rabbit. The squirrel does not visit the rabbit. If the rabbit visits the squirrel then the rabbit is kind. If the squirrel chases the rabbit then the squirrel is red. If someone visits the rabbit then they are cold. If someone chases the rabbit then they do not see the squirrel. If someone is young and they do not visit the squirrel then they chase the rabbit. If someone is young and not red then they chase the squirrel. If someone chases the squirrel and the squirrel is kind then the squirrel is green. If someone is cold and they do not chase the squirrel then they are not kind.
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is not red.
("rabbit" "is" "red" "-")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The squirrel does not visit the rabbit.
("squirrel" "visits" "rabbit" "-")
If the rabbit visits the squirrel then the rabbit is kind.
((("rabbit" "visits" "squirrel" "+")) -> ("rabbit" "is" "kind" "+"))
If the squirrel chases the rabbit then the squirrel is red.
((("squirrel" "chases" "rabbit" "+")) -> ("squirrel" "is" "red" "+"))
If someone visits the rabbit then they are cold.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "cold" "+"))
If someone chases the rabbit then they do not see the squirrel.
((("someone" "chases" "rabbit" "+")) -> ("someone" "sees" "squirrel" "-"))
If someone is young and they do not visit the squirrel then they chase the rabbit.
((("someone" "is" "young" "+") ("someone" "visits" "squirrel" "~")) -> ("someone" "chases" "rabbit" "+"))
If someone is young and not red then they chase the squirrel.
((("someone" "is" "young" "+") ("someone" "is" "red" "~")) -> ("someone" "chases" "squirrel" "+"))
If someone chases the squirrel and the squirrel is kind then the squirrel is green.
((("someone" "chases" "squirrel" "+") ("squirrel" "is" "kind" "+")) -> ("squirrel" "is" "green" "+"))
If someone is cold and they do not chase the squirrel then they are not kind.
((("someone" "is" "cold" "+") ("someone" "chases" "squirrel" "~")) -> ("someone" "is" "kind" "-"))
The squirrel does not chase the rabbit.
True
1
proof
[(triple8)]
("squirrel" "chases" "rabbit" "-")
triple8
The rabbit is not green.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "green" "-")
triple3
The squirrel is green.
True
3
proof
[(((triple1 triple9) -> rule7) OR ((((triple5 triple4) -> rule6) triple9) -> rule7))]
("squirrel" "is" "green" "+")
((triple1 triple9) -> (rule7 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((((triple5 triple4) -> (rule6 % int2)) triple9) -> (rule7 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2
The squirrel is not green.
False
3
inv-proof
[(((triple1 triple9) -> rule7) OR ((((triple5 triple4) -> rule6) triple9) -> rule7))]
("squirrel" "is" "green" "-")
((triple1 triple9) -> (rule7 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((((triple5 triple4) -> (rule6 % int2)) triple9) -> (rule7 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2
The squirrel is not cold.
Unknown
inv-rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "cold" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The rabbit chases the squirrel.[(triple1 OR ((triple5 triple4) -> rule6))] The rabbit is cold.[(triple2)] The rabbit is green.[(triple3)] The rabbit is not red.[(triple4)] The rabbit is young.[(triple5)] The rabbit sees the squirrel.[(triple6)] The rabbit visits the squirrel.[(triple7)] The squirrel does not chase the rabbit.[(triple8)] The squirrel does not visit the rabbit.[(triple12)] The squirrel is kind.[(triple9)] The squirrel is young.[(triple10)] The squirrel sees the rabbit.[(triple11)] @1: The rabbit is kind.[(((triple7) -> rule1))] The squirrel is green.[(((triple1 triple9) -> rule7) OR ((((triple5 triple4) -> rule6) triple9) -> rule7))]
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple1
((triple5 triple4) -> (rule6 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
The rabbit is green.
("rabbit" "is" "green" "+")
triple3
The rabbit is not red.
("rabbit" "is" "red" "-")
triple4
The rabbit is young.
("rabbit" "is" "young" "+")
triple5
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple6
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple7
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
triple8
The squirrel does not visit the rabbit.
("squirrel" "visits" "rabbit" "-")
triple12
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple9
The squirrel is young.
("squirrel" "is" "young" "+")
triple10
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple11
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple7) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((triple1 triple9) -> (rule7 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((((triple5 triple4) -> (rule6 % int2)) triple9) -> (rule7 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2