The bear is red. The bear is young. The bear needs the mouse. The cow likes the rabbit. The cow needs the mouse. The cow visits the bear. The cow visits the mouse. The cow visits the rabbit. The mouse is rough. The mouse visits the bear. The mouse does not visit the cow. The rabbit visits the mouse. If someone likes the mouse then the mouse likes the rabbit. If the rabbit likes the cow then the cow needs the mouse. If someone visits the bear and they need the bear then the bear does not like the cow. If someone likes the rabbit then they are red. If someone is red and they like the rabbit then they like the mouse. If someone likes the rabbit and they are rough then they are blue. If the bear does not like the cow then the bear is rough. If someone visits the cow then they do not need the cow. If someone needs the mouse and they are not blue then they visit the cow.
The bear is red.
("bear" "is" "red" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If someone likes the mouse then the mouse likes the rabbit.
((("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "rabbit" "+"))
If the rabbit likes the cow then the cow needs the mouse.
((("rabbit" "likes" "cow" "+")) -> ("cow" "needs" "mouse" "+"))
If someone visits the bear and they need the bear then the bear does not like the cow.
((("someone" "visits" "bear" "+") ("someone" "needs" "bear" "+")) -> ("bear" "likes" "cow" "-"))
If someone likes the rabbit then they are red.
((("someone" "likes" "rabbit" "+")) -> ("someone" "is" "red" "+"))
If someone is red and they like the rabbit then they like the mouse.
((("someone" "is" "red" "+") ("someone" "likes" "rabbit" "+")) -> ("someone" "likes" "mouse" "+"))
If someone likes the rabbit and they are rough then they are blue.
((("someone" "likes" "rabbit" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If the bear does not like the cow then the bear is rough.
((("bear" "likes" "cow" "~")) -> ("bear" "is" "rough" "+"))
If someone visits the cow then they do not need the cow.
((("someone" "visits" "cow" "+")) -> ("someone" "needs" "cow" "-"))
If someone needs the mouse and they are not blue then they visit the cow.
((("someone" "needs" "mouse" "+") ("someone" "is" "blue" "~")) -> ("someone" "visits" "cow" "+"))
The bear is red.
True
1
proof
[(triple1)]
("bear" "is" "red" "+")
triple1
The cow does not like the rabbit.
False
1
inv-proof
[(triple4)]
("cow" "likes" "rabbit" "-")
triple4
The cow is red.
True
2
proof
[(((triple4) -> rule4))]
("cow" "is" "red" "+")
((triple4) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple4) -> rule4))]
("cow" "is" "red" "-")
((triple4) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the mouse.
True
4
proof
[(((((triple4) -> rule4) triple4) -> rule5))]
("cow" "likes" "mouse" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow does not like the mouse.
False
4
inv-proof
[(((((triple4) -> rule4) triple4) -> rule5))]
("cow" "likes" "mouse" "-")
((((triple4) -> (rule4 % int2)) triple4) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The mouse likes the rabbit.
True
5
proof
[(((((((triple4) -> rule4) triple4) -> rule5)) -> rule1))]
("mouse" "likes" "rabbit" "+")
((((((triple4) -> (rule4 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The mouse does not like the rabbit.
False
5
inv-proof
[(((((((triple4) -> rule4) triple4) -> rule5)) -> rule1))]
("mouse" "likes" "rabbit" "-")
((((((triple4) -> (rule4 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The mouse is red.
True
6
proof
[(((((((((triple4) -> rule4) triple4) -> rule5)) -> rule1)) -> rule4))]
("mouse" "is" "red" "+")
((((((((triple4) -> (rule4 % int4)) triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The mouse is not red.
False
6
inv-proof
[(((((((((triple4) -> rule4) triple4) -> rule5)) -> rule1)) -> rule4))]
("mouse" "is" "red" "-")
((((((((triple4) -> (rule4 % int4)) triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The mouse likes the mouse.
True
12
proof
[(((((((((((triple4) -> rule4) triple4) -> rule5)) -> rule1)) -> rule4) ((((((triple4) -> rule4) triple4) -> rule5)) -> rule1)) -> rule5))]
("mouse" "likes" "mouse" "+")
((((((((((triple4) -> (rule4 % int5)) triple4) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((((triple4) -> (rule4 % int5)) triple4) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int4
The cow is red.
("cow" "is" "red" "+")
int5
The mouse does not like the mouse.
False
12
inv-proof
[(((((((((((triple4) -> rule4) triple4) -> rule5)) -> rule1)) -> rule4) ((((((triple4) -> rule4) triple4) -> rule5)) -> rule1)) -> rule5))]
("mouse" "likes" "mouse" "-")
((((((((((triple4) -> (rule4 % int5)) triple4) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((((triple4) -> (rule4 % int5)) triple4) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int4
The cow is red.
("cow" "is" "red" "+")
int5
The rabbit does not like the mouse.
Unknown
inv-rconc
[@1: The rabbit likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "likes" "mouse" "-")
The bear likes the mouse.
Unknown
rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "likes" "mouse" "+")
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cow" "visits" "cow" "-")
The rabbit visits the cow.
Unknown
rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("rabbit" "visits" "cow" "+")
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "is" "rough" "-")
The rabbit is blue.
Unknown
rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "blue" "+")
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 likes the cow.
Unknown
random
[@0: The mouse likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cow" "+")
The bear does not need the rabbit.
Unknown
inv-random
[@0: The bear needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "rabbit" "-")
The rabbit likes the cow.
Unknown
random
[@0: The rabbit likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cow" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The bear is red.[(triple1)] The bear is young.[(triple2)] The bear needs the mouse.[(triple3)] The cow likes the rabbit.[(triple4)] The cow needs the mouse.[(triple5)] The cow visits the bear.[(triple6)] The cow visits the mouse.[(triple7)] The cow visits the rabbit.[(triple8)] The mouse does not visit the cow.[(triple11)] The mouse is rough.[(triple9)] The mouse visits the bear.[(triple10)] The rabbit visits the mouse.[(triple12)] @1: The cow is red.[(((triple4) -> rule4))] @2: The cow likes the mouse.[(((((triple4) -> rule4) triple4) -> rule5))] @3: The mouse likes the rabbit.[(((((((triple4) -> rule4) triple4) -> rule5)) -> rule1))] @4: The mouse is blue.[(((((((((triple4) -> rule4) triple4) -> rule5)) -> rule1) triple9) -> rule6))] The mouse is red.[(((((((((triple4) -> rule4) triple4) -> rule5)) -> rule1)) -> rule4))] @5: The mouse likes the mouse.[(((((((((((triple4) -> rule4) triple4) -> rule5)) -> rule1)) -> rule4) ((((((triple4) -> rule4) triple4) -> rule5)) -> rule1)) -> rule5))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple5
The cow visits the bear.
("cow" "visits" "bear" "+")
triple6
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple7
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple8
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
triple11
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple10
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple12
The cow is red.
("cow" "is" "red" "+")
((triple4) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule5 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((((triple4) -> (rule4 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
((((((((triple4) -> (rule4 % int4)) triple4) -> (rule5 % int3))) -> (rule1 % int2)) triple9) -> (rule6 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
((((((((triple4) -> (rule4 % int4)) triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((((((triple4) -> (rule4 % int5)) triple4) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((((triple4) -> (rule4 % int5)) triple4) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int4
The cow is red.
("cow" "is" "red" "+")
int5