The dog is blue. The dog needs the mouse. The dog needs the rabbit. The mouse needs the rabbit. The mouse needs the squirrel. The rabbit chases the dog. The rabbit chases the squirrel. The rabbit is kind. The rabbit is red. The rabbit is rough. The squirrel chases the dog. The squirrel needs the dog. If something sees the rabbit then it sees the dog. If something sees the mouse then the mouse sees the dog. If something is kind then it is green. If something chases the dog and it is green then it needs the dog. If something chases the squirrel and it is green then it chases the dog. If something sees the dog and the dog chases the mouse then the mouse is green. If something chases the squirrel then the squirrel needs the dog. If something sees the dog and the dog is red then the dog needs the mouse.
The dog is blue.
("dog" "is" "blue" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
If something sees the rabbit then it sees the dog.
((("something" "sees" "rabbit" "+")) -> ("something" "sees" "dog" "+"))
If something sees the mouse then the mouse sees the dog.
((("something" "sees" "mouse" "+")) -> ("mouse" "sees" "dog" "+"))
If something is kind then it is green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something chases the dog and it is green then it needs the dog.
((("something" "chases" "dog" "+") ("something" "is" "green" "+")) -> ("something" "needs" "dog" "+"))
If something chases the squirrel and it is green then it chases the dog.
((("something" "chases" "squirrel" "+") ("something" "is" "green" "+")) -> ("something" "chases" "dog" "+"))
If something sees the dog and the dog chases the mouse then the mouse is green.
((("something" "sees" "dog" "+") ("dog" "chases" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If something chases the squirrel then the squirrel needs the dog.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "needs" "dog" "+"))
If something sees the dog and the dog is red then the dog needs the mouse.
((("something" "sees" "dog" "+") ("dog" "is" "red" "+")) -> ("dog" "needs" "mouse" "+"))
The rabbit is kind.
True
1
proof
[(triple8)]
("rabbit" "is" "kind" "+")
triple8
The dog does not need the rabbit.
False
1
inv-proof
[(triple3)]
("dog" "needs" "rabbit" "-")
triple3
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "chases" "dog" "-")
The dog chases the squirrel.
Unknown
random
[@0: The dog chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "squirrel" "+")
@0: The dog is blue.[(triple1)] The dog needs the mouse.[(triple2)] The dog needs the rabbit.[(triple3)] The mouse needs the rabbit.[(triple4)] The mouse needs the squirrel.[(triple5)] The rabbit chases the dog.[(triple6 OR ((triple7 ((triple8) -> rule3)) -> rule5))] The rabbit chases the squirrel.[(triple7)] The rabbit is kind.[(triple8)] The rabbit is red.[(triple9)] The rabbit is rough.[(triple10)] The squirrel chases the dog.[(triple11)] The squirrel needs the dog.[(triple12 OR ((triple7) -> rule7))] @1: The rabbit is green.[(((triple8) -> rule3))] @2: The rabbit needs the dog.[(((triple6 ((triple8) -> rule3)) -> rule4) OR ((((triple7 ((triple8) -> rule3)) -> rule5) ((triple8) -> rule3)) -> rule4))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple4
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple5
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple6
((triple7 ((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple8
The rabbit is red.
("rabbit" "is" "red" "+")
triple9
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple10
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple11
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple12
((triple7) -> (rule7 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple8) -> (rule3 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
((triple6 ((triple8) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((((triple7 ((triple8) -> (rule3 % int3))) -> (rule5 % int2)) ((triple8) -> (rule3 % int3))) -> (rule4 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3