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