The bear chases the dog. The bear chases the lion. The bear is kind. The bear needs the rabbit. The dog chases the lion. The dog is blue. The dog is cold. The dog needs the lion. The lion chases the dog. The lion visits the rabbit. The rabbit is kind. The rabbit needs the dog. If something visits the lion then it is young. If something needs the dog then the dog visits the lion. If the dog chases the rabbit then the rabbit chases the bear. If something is young then it chases the bear. If something visits the bear then the bear visits the rabbit. If something needs the dog and the dog chases the bear then it is young. If something needs the lion and it needs the rabbit then the rabbit needs the dog. If something needs the lion then the lion is young.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
If something visits the lion then it is young.
((("something" "visits" "lion" "+")) -> ("something" "is" "young" "+"))
If something needs the dog then the dog visits the lion.
((("something" "needs" "dog" "+")) -> ("dog" "visits" "lion" "+"))
If the dog chases the rabbit then the rabbit chases the bear.
((("dog" "chases" "rabbit" "+")) -> ("rabbit" "chases" "bear" "+"))
If something is young then it chases the bear.
((("something" "is" "young" "+")) -> ("something" "chases" "bear" "+"))
If something visits the bear then the bear visits the rabbit.
((("something" "visits" "bear" "+")) -> ("bear" "visits" "rabbit" "+"))
If something needs the dog and the dog chases the bear then it is young.
((("something" "needs" "dog" "+") ("dog" "chases" "bear" "+")) -> ("something" "is" "young" "+"))
If something needs the lion and it needs the rabbit then the rabbit needs the dog.
((("something" "needs" "lion" "+") ("something" "needs" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
If something needs the lion then the lion is young.
((("something" "needs" "lion" "+")) -> ("lion" "is" "young" "+"))
The bear needs the rabbit.
True
1
proof
[(triple4)]
("bear" "needs" "rabbit" "+")
triple4
The dog is not blue.
False
1
inv-proof
[(triple6)]
("dog" "is" "blue" "-")
triple6
The lion is young.
True
2
proof
[(((triple8) -> rule8))]
("lion" "is" "young" "+")
((triple8) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The dog does not visit the lion.
False
2
inv-proof
[(((triple12) -> rule2))]
("dog" "visits" "lion" "-")
((triple12) -> (rule2 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog is young.
True
3
proof
[(((((triple12) -> rule2)) -> rule1))]
("dog" "is" "young" "+")
((((triple12) -> (rule2 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The lion does not chase the bear.
False
3
inv-proof
[(((((triple8) -> rule8)) -> rule4))]
("lion" "chases" "bear" "-")
((((triple8) -> (rule8 % int2))) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The dog chases the bear.
True
4
proof
[(((((((triple12) -> rule2)) -> rule1)) -> rule4))]
("dog" "chases" "bear" "+")
((((((triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3
The dog does not chase the bear.
False
4
inv-proof
[(((((((triple12) -> rule2)) -> rule1)) -> rule4))]
("dog" "chases" "bear" "-")
((((((triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3
The rabbit is young.
True
6
proof
[(((triple12 ((((((triple12) -> rule2)) -> rule1)) -> rule4)) -> rule6))]
("rabbit" "is" "young" "+")
((triple12 ((((((triple12) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog visits the lion.
("dog" "visits" "lion" "+")
int4
The rabbit is not young.
False
6
inv-proof
[(((triple12 ((((((triple12) -> rule2)) -> rule1)) -> rule4)) -> rule6))]
("rabbit" "is" "young" "-")
((triple12 ((((((triple12) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog visits the lion.
("dog" "visits" "lion" "+")
int4
The rabbit chases the bear.
True
7
proof
[(((((triple12 ((((((triple12) -> rule2)) -> rule1)) -> rule4)) -> rule6)) -> rule4))]
("rabbit" "chases" "bear" "+")
((((triple12 ((((((triple12) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The dog chases the bear.
("dog" "chases" "bear" "+")
int3
The dog is young.
("dog" "is" "young" "+")
int4
The dog visits the lion.
("dog" "visits" "lion" "+")
int5
The rabbit does not chase the bear.
False
7
inv-proof
[(((((triple12 ((((((triple12) -> rule2)) -> rule1)) -> rule4)) -> rule6)) -> rule4))]
("rabbit" "chases" "bear" "-")
((((triple12 ((((((triple12) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The dog chases the bear.
("dog" "chases" "bear" "+")
int3
The dog is young.
("dog" "is" "young" "+")
int4
The dog visits the lion.
("dog" "visits" "lion" "+")
int5
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "young" "-")
The bear chases the bear.
Unknown
rconc
[@2: The bear chases the bear.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("bear" "chases" "bear" "+")
The bear does not visit the rabbit.
Unknown
inv-rconc
[@1: The bear visits the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "visits" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The bear needs the lion.
Unknown
random
[@0: The bear needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "lion" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The lion needs the bear.
Unknown
random
[@0: The lion needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bear" "+")
@0: The bear chases the dog.[(triple1)] The bear chases the lion.[(triple2)] The bear is kind.[(triple3)] The bear needs the rabbit.[(triple4)] The dog chases the lion.[(triple5)] The dog is blue.[(triple6)] The dog is cold.[(triple7)] The dog needs the lion.[(triple8)] The lion chases the dog.[(triple9)] The lion visits the rabbit.[(triple10)] The rabbit is kind.[(triple11)] The rabbit needs the dog.[(triple12)] @1: The dog visits the lion.[(((triple12) -> rule2))] The lion is young.[(((triple8) -> rule8))] @2: The dog is young.[(((((triple12) -> rule2)) -> rule1))] The lion chases the bear.[(((((triple8) -> rule8)) -> rule4))] @3: The dog chases the bear.[(((((((triple12) -> rule2)) -> rule1)) -> rule4))] @4: The rabbit is young.[(((triple12 ((((((triple12) -> rule2)) -> rule1)) -> rule4)) -> rule6))] @5: The rabbit chases the bear.[(((((triple12 ((((((triple12) -> rule2)) -> rule1)) -> rule4)) -> rule6)) -> rule4))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear chases the lion.
("bear" "chases" "lion" "+")
triple2
The bear is kind.
("bear" "is" "kind" "+")
triple3
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple4
The dog chases the lion.
("dog" "chases" "lion" "+")
triple5
The dog is blue.
("dog" "is" "blue" "+")
triple6
The dog is cold.
("dog" "is" "cold" "+")
triple7
The dog needs the lion.
("dog" "needs" "lion" "+")
triple8
The lion chases the dog.
("lion" "chases" "dog" "+")
triple9
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple10
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple11
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple12
The dog visits the lion.
("dog" "visits" "lion" "+")
((triple12) -> (rule2 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((triple8) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple12) -> (rule2 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The lion chases the bear.
("lion" "chases" "bear" "+")
((((triple8) -> (rule8 % int2))) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The dog chases the bear.
("dog" "chases" "bear" "+")
((((((triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3
The rabbit is young.
("rabbit" "is" "young" "+")
((triple12 ((((((triple12) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog visits the lion.
("dog" "visits" "lion" "+")
int4
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((((triple12 ((((((triple12) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The dog chases the bear.
("dog" "chases" "bear" "+")
int3
The dog is young.
("dog" "is" "young" "+")
int4
The dog visits the lion.
("dog" "visits" "lion" "+")
int5