The bear is red. The cow does not need the rabbit. The rabbit is nice. The squirrel is not round. If something chases the bear then the bear is not round. If something is red then it chases the cow. If something needs the rabbit then the rabbit needs the squirrel. If something needs the rabbit and it is nice then it needs the cow. If something chases the cow then it chases the bear. If something needs the squirrel then it is young. If something is rough and it does not need the cow then the cow does not like the rabbit. If something chases the rabbit and it does not like the rabbit then it chases the squirrel.
The bear is red.
("bear" "is" "red" "+")
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The squirrel is not round.
("squirrel" "is" "round" "-")
If something chases the bear then the bear is not round.
((("something" "chases" "bear" "+")) -> ("bear" "is" "round" "-"))
If something is red then it chases the cow.
((("something" "is" "red" "+")) -> ("something" "chases" "cow" "+"))
If something needs the rabbit then the rabbit needs the squirrel.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "needs" "squirrel" "+"))
If something needs the rabbit and it is nice then it needs the cow.
((("something" "needs" "rabbit" "+") ("something" "is" "nice" "+")) -> ("something" "needs" "cow" "+"))
If something chases the cow then it chases the bear.
((("something" "chases" "cow" "+")) -> ("something" "chases" "bear" "+"))
If something needs the squirrel then it is young.
((("something" "needs" "squirrel" "+")) -> ("something" "is" "young" "+"))
If something is rough and it does not need the cow then the cow does not like the rabbit.
((("something" "is" "rough" "+") ("something" "needs" "cow" "~")) -> ("cow" "likes" "rabbit" "-"))
If something chases the rabbit and it does not like the rabbit then it chases the squirrel.
((("something" "chases" "rabbit" "+") ("something" "likes" "rabbit" "~")) -> ("something" "chases" "squirrel" "+"))
The cow does not need the rabbit.
True
1
proof
[(triple2)]
("cow" "needs" "rabbit" "-")
triple2
The squirrel is round.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "round" "+")
triple4
The bear chases the cow.
True
2
proof
[(((triple1) -> rule2))]
("bear" "chases" "cow" "+")
((triple1) -> (rule2 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear does not chase the cow.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "chases" "cow" "-")
((triple1) -> (rule2 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear chases the bear.
True
3
proof
[(((((triple1) -> rule2)) -> rule5))]
("bear" "chases" "bear" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear does not chase the bear.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5))]
("bear" "chases" "bear" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear is not round.
True
4
proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule1))]
("bear" "is" "round" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bear is not round.
("bear" "is" "round" "-")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
The bear is round.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule1))]
("bear" "is" "round" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bear is not round.
("bear" "is" "round" "-")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
The bear does not chase the squirrel.
Unknown
inv-rconc
[@1: The bear chases the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "chases" "squirrel" "-")
The squirrel chases the bear.
Unknown
rconc
[@2: The squirrel chases the bear.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("squirrel" "chases" "bear" "+")
The rabbit is not young.
Unknown
inv-rconc
[@2: The rabbit is young.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("rabbit" "is" "young" "-")
The squirrel chases the cow.
Unknown
rconc
[@1: The squirrel chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "cow" "+")
The bear does not like the squirrel.
Unknown
inv-random
[@0: The bear likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "squirrel" "-")
The cow needs the bear.
Unknown
random
[@0: The cow needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bear" "+")
The cow does not like the bear.
Unknown
inv-random
[@0: The cow likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "bear" "-")
The squirrel needs the rabbit.
Unknown
random
[@0: The squirrel needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "rabbit" "+")
@0: The bear is red.[(triple1)] The cow does not need the rabbit.[(triple2)] The rabbit is nice.[(triple3)] The squirrel is not round.[(triple4)] @1: The bear chases the cow.[(((triple1) -> rule2))] @2: The bear chases the bear.[(((((triple1) -> rule2)) -> rule5))] @3: The bear is not round.[(((((((triple1) -> rule2)) -> rule5)) -> rule1))]
The bear is red.
("bear" "is" "red" "+")
triple1
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
triple2
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple3
The squirrel is not round.
("squirrel" "is" "round" "-")
triple4
The bear chases the cow.
("bear" "chases" "cow" "+")
((triple1) -> (rule2 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear is not round.
("bear" "is" "round" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The bear is not round.
("bear" "is" "round" "-")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3