The bear eats the cow. The bear eats the mouse. The bear is round. The cow chases the dog. The cow does not eat the bear. The cow is round. The cow needs the mouse. The dog is red. The mouse chases the dog. The mouse eats the bear. If something chases the bear and it eats the dog then the dog chases the cow. If something chases the bear then the bear chases the dog. If something is red and not nice then it is round. If something chases the dog then it needs the dog. If something is cold and not red then it does not eat the mouse. If something eats the mouse and the mouse is kind then the mouse eats the cow. If something needs the dog then it chases the bear.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is round.
("bear" "is" "round" "+")
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow does not eat the bear.
("cow" "eats" "bear" "-")
The cow is round.
("cow" "is" "round" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The dog is red.
("dog" "is" "red" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
If something chases the bear and it eats the dog then the dog chases the cow.
((("something" "chases" "bear" "+") ("something" "eats" "dog" "+")) -> ("dog" "chases" "cow" "+"))
If something chases the bear then the bear chases the dog.
((("something" "chases" "bear" "+")) -> ("bear" "chases" "dog" "+"))
If something is red and not nice then it is round.
((("something" "is" "red" "+") ("something" "is" "nice" "~")) -> ("something" "is" "round" "+"))
If something chases the dog then it needs the dog.
((("something" "chases" "dog" "+")) -> ("something" "needs" "dog" "+"))
If something is cold and not red then it does not eat the mouse.
((("something" "is" "cold" "+") ("something" "is" "red" "~")) -> ("something" "eats" "mouse" "-"))
If something eats the mouse and the mouse is kind then the mouse eats the cow.
((("something" "eats" "mouse" "+") ("mouse" "is" "kind" "+")) -> ("mouse" "eats" "cow" "+"))
If something needs the dog then it chases the bear.
((("something" "needs" "dog" "+")) -> ("something" "chases" "bear" "+"))
The cow chases the dog.
True
1
proof
[(triple4)]
("cow" "chases" "dog" "+")
triple4
The bear does not eat the mouse.
False
1
inv-proof
[(triple2)]
("bear" "eats" "mouse" "-")
triple2
The mouse needs the dog.
True
2
proof
[(((triple9) -> rule4))]
("mouse" "needs" "dog" "+")
((triple9) -> (rule4 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The cow does not need the dog.
False
2
inv-proof
[(((triple4) -> rule4))]
("cow" "needs" "dog" "-")
((triple4) -> (rule4 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The cow chases the bear.
True
3
proof
[(((((triple4) -> rule4)) -> rule7))]
("cow" "chases" "bear" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The mouse does not chase the bear.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule7))]
("mouse" "chases" "bear" "-")
((((triple9) -> (rule4 % int2))) -> (rule7 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The bear chases the dog.
True
4
proof
[(((((((triple4) -> rule4)) -> rule7)) -> rule2) OR ((((((triple9) -> rule4)) -> rule7)) -> rule2))]
("bear" "chases" "dog" "+")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cow needs the dog.
("cow" "needs" "dog" "+")
int3
((((((triple9) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The bear does not chase the dog.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule7)) -> rule2) OR ((((((triple9) -> rule4)) -> rule7)) -> rule2))]
("bear" "chases" "dog" "-")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cow needs the dog.
("cow" "needs" "dog" "+")
int3
((((((triple9) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The bear needs the dog.
True
5
proof
[(((((((((triple4) -> rule4)) -> rule7)) -> rule2)) -> rule4) OR ((((((((triple9) -> rule4)) -> rule7)) -> rule2)) -> rule4))]
("bear" "needs" "dog" "+")
((((((((triple4) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear chases the dog.
("bear" "chases" "dog" "+")
int2
The cow chases the bear.
("cow" "chases" "bear" "+")
int3
The cow needs the dog.
("cow" "needs" "dog" "+")
int4
((((((((triple9) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear chases the dog.
("bear" "chases" "dog" "+")
int2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The bear does not need the dog.
False
5
inv-proof
[(((((((((triple4) -> rule4)) -> rule7)) -> rule2)) -> rule4) OR ((((((((triple9) -> rule4)) -> rule7)) -> rule2)) -> rule4))]
("bear" "needs" "dog" "-")
((((((((triple4) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear chases the dog.
("bear" "chases" "dog" "+")
int2
The cow chases the bear.
("cow" "chases" "bear" "+")
int3
The cow needs the dog.
("cow" "needs" "dog" "+")
int4
((((((((triple9) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear chases the dog.
("bear" "chases" "dog" "+")
int2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The bear chases the bear.
True
6
proof
[(((((((((((triple4) -> rule4)) -> rule7)) -> rule2)) -> rule4)) -> rule7) OR ((((((((((triple9) -> rule4)) -> rule7)) -> rule2)) -> rule4)) -> rule7))]
("bear" "chases" "bear" "+")
((((((((((triple4) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear chases the dog.
("bear" "chases" "dog" "+")
int3
The cow chases the bear.
("cow" "chases" "bear" "+")
int4
The cow needs the dog.
("cow" "needs" "dog" "+")
int5
((((((((((triple9) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear chases the dog.
("bear" "chases" "dog" "+")
int3
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int4
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int5
The bear does not chase the bear.
False
6
inv-proof
[(((((((((((triple4) -> rule4)) -> rule7)) -> rule2)) -> rule4)) -> rule7) OR ((((((((((triple9) -> rule4)) -> rule7)) -> rule2)) -> rule4)) -> rule7))]
("bear" "chases" "bear" "-")
((((((((((triple4) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear chases the dog.
("bear" "chases" "dog" "+")
int3
The cow chases the bear.
("cow" "chases" "bear" "+")
int4
The cow needs the dog.
("cow" "needs" "dog" "+")
int5
((((((((((triple9) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear chases the dog.
("bear" "chases" "dog" "+")
int3
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int4
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int5
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "round" "-")
The dog chases the bear.
Unknown
rconc
[@2: The dog chases the bear.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("dog" "chases" "bear" "+")
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "dog" "-")
The mouse eats the cow.
Unknown
rconc
[@1: The mouse eats the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "cow" "+")
The dog does not chase the cow.
Unknown
inv-rconc
[@1: The dog chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "cow" "-")
The mouse is round.
Unknown
rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "round" "+")
The dog does not eat the bear.
Unknown
inv-random
[@0: The dog eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "bear" "-")
The dog chases the mouse.
Unknown
random
[@0: The dog chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "mouse" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog needs the cow.
Unknown
random
[@0: The dog needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cow" "+")
@0: The bear eats the cow.[(triple1)] The bear eats the mouse.[(triple2)] The bear is round.[(triple3)] The cow chases the dog.[(triple4)] The cow does not eat the bear.[(triple5)] The cow is round.[(triple6)] The cow needs the mouse.[(triple7)] The dog is red.[(triple8)] The mouse chases the dog.[(triple9)] The mouse eats the bear.[(triple10)] @1: The cow needs the dog.[(((triple4) -> rule4))] The mouse needs the dog.[(((triple9) -> rule4))] @2: The cow chases the bear.[(((((triple4) -> rule4)) -> rule7))] The mouse chases the bear.[(((((triple9) -> rule4)) -> rule7))] @3: The bear chases the dog.[(((((((triple4) -> rule4)) -> rule7)) -> rule2) OR ((((((triple9) -> rule4)) -> rule7)) -> rule2))] @4: The bear needs the dog.[(((((((((triple4) -> rule4)) -> rule7)) -> rule2)) -> rule4) OR ((((((((triple9) -> rule4)) -> rule7)) -> rule2)) -> rule4))] @5: The bear chases the bear.[(((((((((((triple4) -> rule4)) -> rule7)) -> rule2)) -> rule4)) -> rule7) OR ((((((((((triple9) -> rule4)) -> rule7)) -> rule2)) -> rule4)) -> rule7))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The cow chases the dog.
("cow" "chases" "dog" "+")
triple4
The cow does not eat the bear.
("cow" "eats" "bear" "-")
triple5
The cow is round.
("cow" "is" "round" "+")
triple6
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple7
The dog is red.
("dog" "is" "red" "+")
triple8
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple9
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple10
The cow needs the dog.
("cow" "needs" "dog" "+")
((triple4) -> (rule4 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((triple9) -> (rule4 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((((triple9) -> (rule4 % int2))) -> (rule7 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The bear chases the dog.
("bear" "chases" "dog" "+")
((((((triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cow needs the dog.
("cow" "needs" "dog" "+")
int3
((((((triple9) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The bear needs the dog.
("bear" "needs" "dog" "+")
((((((((triple4) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear chases the dog.
("bear" "chases" "dog" "+")
int2
The cow chases the bear.
("cow" "chases" "bear" "+")
int3
The cow needs the dog.
("cow" "needs" "dog" "+")
int4
((((((((triple9) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear chases the dog.
("bear" "chases" "dog" "+")
int2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
((((((((((triple4) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear chases the dog.
("bear" "chases" "dog" "+")
int3
The cow chases the bear.
("cow" "chases" "bear" "+")
int4
The cow needs the dog.
("cow" "needs" "dog" "+")
int5
((((((((((triple9) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear chases the dog.
("bear" "chases" "dog" "+")
int3
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int4
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int5