The bear needs the rabbit. The bear sees the rabbit. The dog is young. The dog sees the bear. The rabbit needs the bear. The rabbit needs the dog. The rabbit sees the dog. If something is young and it sees the dog then the dog is blue. If something is young then it chases the bear. If something sees the dog and the dog does not need the rabbit then it needs the dog. If something chases the dog then the dog is not red. If the bear is blue then the bear does not chase the dog. If something chases the bear then it needs the bear.
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The dog is young.
("dog" "is" "young" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If something is young and it sees the dog then the dog is blue.
((("something" "is" "young" "+") ("something" "sees" "dog" "+")) -> ("dog" "is" "blue" "+"))
If something is young then it chases the bear.
((("something" "is" "young" "+")) -> ("something" "chases" "bear" "+"))
If something sees the dog and the dog does not need the rabbit then it needs the dog.
((("something" "sees" "dog" "+") ("dog" "needs" "rabbit" "~")) -> ("something" "needs" "dog" "+"))
If something chases the dog then the dog is not red.
((("something" "chases" "dog" "+")) -> ("dog" "is" "red" "-"))
If the bear is blue then the bear does not chase the dog.
((("bear" "is" "blue" "+")) -> ("bear" "chases" "dog" "-"))
If something chases the bear then it needs the bear.
((("something" "chases" "bear" "+")) -> ("something" "needs" "bear" "+"))
The dog is young.
True
1
proof
[(triple3)]
("dog" "is" "young" "+")
triple3
The rabbit does not need the bear.
False
1
inv-proof
[(triple5)]
("rabbit" "needs" "bear" "-")
triple5
The dog chases the bear.
True
2
proof
[(((triple3) -> rule2))]
("dog" "chases" "bear" "+")
((triple3) -> (rule2 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The dog does not chase the bear.
False
2
inv-proof
[(((triple3) -> rule2))]
("dog" "chases" "bear" "-")
((triple3) -> (rule2 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The dog needs the bear.
True
3
proof
[(((((triple3) -> rule2)) -> rule6))]
("dog" "needs" "bear" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The dog does not need the bear.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule6))]
("dog" "needs" "bear" "-")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "dog" "-")
The bear chases the bear.
Unknown
rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "chases" "bear" "+")
The bear does not need the dog.
Unknown
inv-rconc
[@1: The bear needs the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "dog" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
The bear does not see the dog.
Unknown
inv-random
[@0: The bear sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "dog" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear needs the rabbit.[(triple1)] The bear sees the rabbit.[(triple2)] The dog is young.[(triple3)] The dog sees the bear.[(triple4)] The rabbit needs the bear.[(triple5)] The rabbit needs the dog.[(triple6)] The rabbit sees the dog.[(triple7)] @1: The dog chases the bear.[(((triple3) -> rule2))] @2: The dog needs the bear.[(((((triple3) -> rule2)) -> rule6))]
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The dog sees the bear.
("dog" "sees" "bear" "+")
triple4
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple5
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple6
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple7
The dog chases the bear.
("dog" "chases" "bear" "+")
((triple3) -> (rule2 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2