The bear sees the rabbit. The cow chases the bear. The cow chases the rabbit. The cow is cold. The cow needs the bear. The cow does not see the mouse. The mouse chases the bear. The mouse is nice. The mouse needs the cow. The rabbit needs the bear. The rabbit does not see the bear. If someone sees the rabbit then they do not chase the cow. If someone is cold and they see the rabbit then the rabbit is red. If someone sees the mouse and they need the rabbit then the rabbit is young. If someone needs the bear then the bear sees the cow. If the rabbit is nice and the rabbit does not need the bear then the rabbit needs the cow. If the bear is red then the bear sees the rabbit. All red people are cold. If someone is cold then they see the rabbit.
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
If someone sees the rabbit then they do not chase the cow.
((("someone" "sees" "rabbit" "+")) -> ("someone" "chases" "cow" "-"))
If someone is cold and they see the rabbit then the rabbit is red.
((("someone" "is" "cold" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
If someone sees the mouse and they need the rabbit then the rabbit is young.
((("someone" "sees" "mouse" "+") ("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If someone needs the bear then the bear sees the cow.
((("someone" "needs" "bear" "+")) -> ("bear" "sees" "cow" "+"))
If the rabbit is nice and the rabbit does not need the bear then the rabbit needs the cow.
((("rabbit" "is" "nice" "+") ("rabbit" "needs" "bear" "~")) -> ("rabbit" "needs" "cow" "+"))
If the bear is red then the bear sees the rabbit.
((("bear" "is" "red" "+")) -> ("bear" "sees" "rabbit" "+"))
All red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they see the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "rabbit" "+"))
The rabbit does not see the bear.
True
1
proof
[(triple11)]
("rabbit" "sees" "bear" "-")
triple11
The mouse does not chase the bear.
False
1
inv-proof
[(triple7)]
("mouse" "chases" "bear" "-")
triple7
The bear sees the cow.
True
2
proof
[(((triple10) -> rule4) OR ((triple5) -> rule4))]
("bear" "sees" "cow" "+")
((triple10) -> (rule4 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
((triple5) -> (rule4 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The cow does not see the rabbit.
False
2
inv-proof
[(((triple4) -> rule8))]
("cow" "sees" "rabbit" "-")
((triple4) -> (rule8 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The rabbit is red.
True
4
proof
[(((triple4 ((triple4) -> rule8)) -> rule2))]
("rabbit" "is" "red" "+")
((triple4 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The rabbit is not red.
False
4
inv-proof
[(((triple4 ((triple4) -> rule8)) -> rule2))]
("rabbit" "is" "red" "-")
((triple4 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The rabbit is cold.
True
5
proof
[(((((triple4 ((triple4) -> rule8)) -> rule2)) -> rule7))]
("rabbit" "is" "cold" "+")
((((triple4 ((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The rabbit is not cold.
False
5
inv-proof
[(((((triple4 ((triple4) -> rule8)) -> rule2)) -> rule7))]
("rabbit" "is" "cold" "-")
((((triple4 ((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The rabbit sees the rabbit.
True
6
proof
[(((((((triple4 ((triple4) -> rule8)) -> rule2)) -> rule7)) -> rule8))]
("rabbit" "sees" "rabbit" "+")
((((((triple4 ((triple4) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The rabbit does not see the rabbit.
False
6
inv-proof
[(((((((triple4 ((triple4) -> rule8)) -> rule2)) -> rule7)) -> rule8))]
("rabbit" "sees" "rabbit" "-")
((((((triple4 ((triple4) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The rabbit does not chase the cow.
True
7
proof
[(((((((((triple4 ((triple4) -> rule8)) -> rule2)) -> rule7)) -> rule8)) -> rule1))]
("rabbit" "chases" "cow" "-")
((((((((triple4 ((triple4) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit does not chase the cow.
("rabbit" "chases" "cow" "-")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int5
The rabbit chases the cow.
False
7
inv-proof
[(((((((((triple4 ((triple4) -> rule8)) -> rule2)) -> rule7)) -> rule8)) -> rule1))]
("rabbit" "chases" "cow" "+")
((((((((triple4 ((triple4) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit does not chase the cow.
("rabbit" "chases" "cow" "-")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int5
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "young" "-")
The rabbit needs the cow.
Unknown
rconc
[@1: The rabbit needs the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "needs" "cow" "+")
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "cold" "-")
The bear is cold.
Unknown
rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "is" "cold" "+")
The mouse does not see the rabbit.
Unknown
inv-rconc
[@2: The mouse sees the rabbit.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("mouse" "sees" "rabbit" "-")
The bear needs the cow.
Unknown
random
[@0: The bear needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cow" "+")
The rabbit does not chase the bear.
Unknown
inv-random
[@0: The rabbit chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "bear" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The cow does not need the rabbit.
Unknown
inv-random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "-")
The rabbit chases the mouse.
Unknown
random
[@0: The rabbit chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "mouse" "+")
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 mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The bear sees the rabbit.[(triple1)] The cow chases the bear.[(triple2)] The cow chases the rabbit.[(triple3)] The cow does not see the mouse.[(triple6)] The cow is cold.[(triple4)] The cow needs the bear.[(triple5)] The mouse chases the bear.[(triple7)] The mouse is nice.[(triple8)] The mouse needs the cow.[(triple9)] The rabbit does not see the bear.[(triple11)] The rabbit needs the bear.[(triple10)] @1: The bear does not chase the cow.[(((triple1) -> rule1))] The bear sees the cow.[(((triple10) -> rule4) OR ((triple5) -> rule4))] The cow sees the rabbit.[(((triple4) -> rule8))] @2: The cow does not chase the cow.[(((((triple4) -> rule8)) -> rule1))] The rabbit is red.[(((triple4 ((triple4) -> rule8)) -> rule2))] @3: The rabbit is cold.[(((((triple4 ((triple4) -> rule8)) -> rule2)) -> rule7))] @4: The rabbit sees the rabbit.[(((((((triple4 ((triple4) -> rule8)) -> rule2)) -> rule7)) -> rule8))] @5: The rabbit does not chase the cow.[(((((((((triple4 ((triple4) -> rule8)) -> rule2)) -> rule7)) -> rule8)) -> rule1))]
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple1
The cow chases the bear.
("cow" "chases" "bear" "+")
triple2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple3
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
triple6
The cow is cold.
("cow" "is" "cold" "+")
triple4
The cow needs the bear.
("cow" "needs" "bear" "+")
triple5
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple9
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
triple11
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple10
The bear does not chase the cow.
("bear" "chases" "cow" "-")
((triple1) -> (rule1 % int1))
The bear does not chase the cow.
("bear" "chases" "cow" "-")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
((triple10) -> (rule4 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
((triple5) -> (rule4 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
((triple4) -> (rule8 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow does not chase the cow.
("cow" "chases" "cow" "-")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The cow does not chase the cow.
("cow" "chases" "cow" "-")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
((triple4 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((triple4 ((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((triple4 ((triple4) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The rabbit does not chase the cow.
("rabbit" "chases" "cow" "-")
((((((((triple4 ((triple4) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit does not chase the cow.
("rabbit" "chases" "cow" "-")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int5