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