The bear chases the rabbit. The cat needs the bear. The cow needs the rabbit. The rabbit visits the cat. If someone needs the rabbit and the rabbit is red then the rabbit needs the cow. If someone chases the rabbit then they visit the cat. If someone needs the cow then the cow chases the bear. If someone visits the cat then the cat needs the cow. If someone chases the cow then they are young. If someone chases the bear then the bear chases the cow. If someone needs the rabbit and the rabbit visits the bear then the rabbit chases the cow. If someone needs the cat then the cat needs the cow.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If someone needs the rabbit and the rabbit is red then the rabbit needs the cow.
((("someone" "needs" "rabbit" "+") ("rabbit" "is" "red" "+")) -> ("rabbit" "needs" "cow" "+"))
If someone chases the rabbit then they visit the cat.
((("someone" "chases" "rabbit" "+")) -> ("someone" "visits" "cat" "+"))
If someone needs the cow then the cow chases the bear.
((("someone" "needs" "cow" "+")) -> ("cow" "chases" "bear" "+"))
If someone visits the cat then the cat needs the cow.
((("someone" "visits" "cat" "+")) -> ("cat" "needs" "cow" "+"))
If someone chases the cow then they are young.
((("someone" "chases" "cow" "+")) -> ("someone" "is" "young" "+"))
If someone chases the bear then the bear chases the cow.
((("someone" "chases" "bear" "+")) -> ("bear" "chases" "cow" "+"))
If someone needs the rabbit and the rabbit visits the bear then the rabbit chases the cow.
((("someone" "needs" "rabbit" "+") ("rabbit" "visits" "bear" "+")) -> ("rabbit" "chases" "cow" "+"))
If someone needs the cat then the cat needs the cow.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "cow" "+"))
The bear chases the rabbit.
True
1
proof
[(triple1)]
("bear" "chases" "rabbit" "+")
triple1
The bear does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "chases" "rabbit" "-")
triple1
The bear visits the cat.
True
2
proof
[(((triple1) -> rule2))]
("bear" "visits" "cat" "+")
((triple1) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear does not visit the cat.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "visits" "cat" "-")
((triple1) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The cow chases the bear.
True
3
proof
[(((((triple4) -> rule4)) -> rule3) OR ((((((triple1) -> rule2)) -> rule4)) -> rule3))]
("cow" "chases" "bear" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The cow does not chase the bear.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule3) OR ((((((triple1) -> rule2)) -> rule4)) -> rule3))]
("cow" "chases" "bear" "-")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear chases the cow.
True
4
proof
[(((((((triple4) -> rule4)) -> rule3)) -> rule6) OR ((((((((triple1) -> rule2)) -> rule4)) -> rule3)) -> rule6))]
("bear" "chases" "cow" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cat needs the cow.
("cat" "needs" "cow" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cat needs the cow.
("cat" "needs" "cow" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
The bear does not chase the cow.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule3)) -> rule6) OR ((((((((triple1) -> rule2)) -> rule4)) -> rule3)) -> rule6))]
("bear" "chases" "cow" "-")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cat needs the cow.
("cat" "needs" "cow" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cat needs the cow.
("cat" "needs" "cow" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "young" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "cat" "+")
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "young" "-")
The rabbit is young.
Unknown
rconc
[@2: The rabbit is young.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("rabbit" "is" "young" "+")
The cat does not chase the cow.
Unknown
inv-random
[@0: The cat chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cow" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The cat does not visit the bear.
Unknown
inv-random
[@0: The cat visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "bear" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
@0: The bear chases the rabbit.[(triple1)] The cat needs the bear.[(triple2)] The cow needs the rabbit.[(triple3)] The rabbit visits the cat.[(triple4)] @1: The bear visits the cat.[(((triple1) -> rule2))] The cat needs the cow.[(((triple4) -> rule4) OR ((((triple1) -> rule2)) -> rule4))] @2: The cow chases the bear.[(((((triple4) -> rule4)) -> rule3) OR ((((((triple1) -> rule2)) -> rule4)) -> rule3))] @3: The bear chases the cow.[(((((((triple4) -> rule4)) -> rule3)) -> rule6) OR ((((((((triple1) -> rule2)) -> rule4)) -> rule3)) -> rule6))] @4: The bear is young.[(((((((((triple4) -> rule4)) -> rule3)) -> rule6)) -> rule5) OR ((((((((((triple1) -> rule2)) -> rule4)) -> rule3)) -> rule6)) -> rule5))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The cat needs the bear.
("cat" "needs" "bear" "+")
triple2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple3
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple4
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple1) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
((triple4) -> (rule4 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The cow chases the bear.
("cow" "chases" "bear" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear chases the cow.
("bear" "chases" "cow" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cat needs the cow.
("cat" "needs" "cow" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cat needs the cow.
("cat" "needs" "cow" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
The bear is young.
("bear" "is" "young" "+")
((((((((triple4) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The cow chases the bear.
("cow" "chases" "bear" "+")
int3
The cat needs the cow.
("cat" "needs" "cow" "+")
int4
((((((((((triple1) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The cow chases the bear.
("cow" "chases" "bear" "+")
int3
The cat needs the cow.
("cat" "needs" "cow" "+")
int4
The bear visits the cat.
("bear" "visits" "cat" "+")
int5