The dog chases the rabbit. The dog is big. The dog is cold. The dog is nice. The dog is young. The dog needs the mouse. The dog needs the rabbit. The dog needs the squirrel. The mouse chases the squirrel. The mouse is cold. The mouse needs the dog. The rabbit sees the mouse. The squirrel chases the rabbit. The squirrel is big. The squirrel needs the dog. If something sees the rabbit then the rabbit chases the dog. If something needs the squirrel then it sees the rabbit. If something chases the dog then the dog sees the squirrel.
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
If something sees the rabbit then the rabbit chases the dog.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "chases" "dog" "+"))
If something needs the squirrel then it sees the rabbit.
((("something" "needs" "squirrel" "+")) -> ("something" "sees" "rabbit" "+"))
If something chases the dog then the dog sees the squirrel.
((("something" "chases" "dog" "+")) -> ("dog" "sees" "squirrel" "+"))
The dog chases the rabbit.
True
1
proof
[(triple1)]
("dog" "chases" "rabbit" "+")
triple1
The dog does not need the rabbit.
False
1
inv-proof
[(triple7)]
("dog" "needs" "rabbit" "-")
triple7
The dog sees the rabbit.
True
2
proof
[(((triple8) -> rule2))]
("dog" "sees" "rabbit" "+")
((triple8) -> (rule2 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog does not see the rabbit.
False
2
inv-proof
[(((triple8) -> rule2))]
("dog" "sees" "rabbit" "-")
((triple8) -> (rule2 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The rabbit chases the dog.
True
3
proof
[(((((triple8) -> rule2)) -> rule1))]
("rabbit" "chases" "dog" "+")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The rabbit does not chase the dog.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule1))]
("rabbit" "chases" "dog" "-")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The dog sees the squirrel.
True
4
proof
[(((((((triple8) -> rule2)) -> rule1)) -> rule3))]
("dog" "sees" "squirrel" "+")
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
The dog does not see the squirrel.
False
4
inv-proof
[(((((((triple8) -> rule2)) -> rule1)) -> rule3))]
("dog" "sees" "squirrel" "-")
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The squirrel sees the rabbit.
Unknown
rconc
[@1: The squirrel sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "rabbit" "+")
The mouse does not see the rabbit.
Unknown
inv-rconc
[@1: The mouse sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "rabbit" "-")
The rabbit sees the dog.
Unknown
random
[@0: The rabbit sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "dog" "+")
The dog does not see the mouse.
Unknown
inv-random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The mouse does not see the squirrel.
Unknown
inv-random
[@0: The mouse sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "squirrel" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The dog chases the rabbit.[(triple1)] The dog is big.[(triple2)] The dog is cold.[(triple3)] The dog is nice.[(triple4)] The dog is young.[(triple5)] The dog needs the mouse.[(triple6)] The dog needs the rabbit.[(triple7)] The dog needs the squirrel.[(triple8)] The mouse chases the squirrel.[(triple9)] The mouse is cold.[(triple10)] The mouse needs the dog.[(triple11)] The rabbit sees the mouse.[(triple12)] The squirrel chases the rabbit.[(triple13)] The squirrel is big.[(triple14)] The squirrel needs the dog.[(triple15)] @1: The dog sees the rabbit.[(((triple8) -> rule2))] @2: The rabbit chases the dog.[(((((triple8) -> rule2)) -> rule1))] @3: The dog sees the squirrel.[(((((((triple8) -> rule2)) -> rule1)) -> rule3))]
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple6
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple7
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple8
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple11
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple12
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple13
The squirrel is big.
("squirrel" "is" "big" "+")
triple14
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple15
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
((triple8) -> (rule2 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3