The bear is nice. The bear sees the cat. The bear visits the cat. The bear visits the mouse. The cat is nice. The cat sees the bear. The cow needs the bear. The cow visits the mouse. The mouse sees the cat. The mouse visits the bear. If someone sees the cow then they visit the cat. If someone is rough then they need the mouse. If someone needs the mouse and they need the bear then the mouse sees the bear. If someone visits the bear then they see the cow. If someone visits the cow and they are nice then the cow is red. If someone visits the mouse and they need the bear then the mouse needs the bear. If someone visits the cat and they visit the bear then the cat visits the mouse. If someone visits the mouse and the mouse is young then they are rough. If someone visits the bear then they are young.
The bear is nice.
("bear" "is" "nice" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If someone sees the cow then they visit the cat.
((("someone" "sees" "cow" "+")) -> ("someone" "visits" "cat" "+"))
If someone is rough then they need the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the mouse and they need the bear then the mouse sees the bear.
((("someone" "needs" "mouse" "+") ("someone" "needs" "bear" "+")) -> ("mouse" "sees" "bear" "+"))
If someone visits the bear then they see the cow.
((("someone" "visits" "bear" "+")) -> ("someone" "sees" "cow" "+"))
If someone visits the cow and they are nice then the cow is red.
((("someone" "visits" "cow" "+") ("someone" "is" "nice" "+")) -> ("cow" "is" "red" "+"))
If someone visits the mouse and they need the bear then the mouse needs the bear.
((("someone" "visits" "mouse" "+") ("someone" "needs" "bear" "+")) -> ("mouse" "needs" "bear" "+"))
If someone visits the cat and they visit the bear then the cat visits the mouse.
((("someone" "visits" "cat" "+") ("someone" "visits" "bear" "+")) -> ("cat" "visits" "mouse" "+"))
If someone visits the mouse and the mouse is young then they are rough.
((("someone" "visits" "mouse" "+") ("mouse" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone visits the bear then they are young.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "young" "+"))
The bear is nice.
True
1
proof
[(triple1)]
("bear" "is" "nice" "+")
triple1
The cat does not see the bear.
False
1
inv-proof
[(triple6)]
("cat" "sees" "bear" "-")
triple6
The mouse sees the cow.
True
2
proof
[(((triple10) -> rule4))]
("mouse" "sees" "cow" "+")
((triple10) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse does not need the bear.
False
3
inv-proof
[(((triple8 triple7) -> rule6))]
("mouse" "needs" "bear" "-")
((triple8 triple7) -> (rule6 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The bear is rough.
True
4
proof
[(((triple4 ((triple10) -> rule9)) -> rule8))]
("bear" "is" "rough" "+")
((triple4 ((triple10) -> (rule9 % int2))) -> (rule8 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The cow is not rough.
False
4
inv-proof
[(((triple8 ((triple10) -> rule9)) -> rule8))]
("cow" "is" "rough" "-")
((triple8 ((triple10) -> (rule9 % int2))) -> (rule8 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The cow needs the mouse.
True
5
proof
[(((((triple8 ((triple10) -> rule9)) -> rule8)) -> rule2))]
("cow" "needs" "mouse" "+")
((((triple8 ((triple10) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The bear does not need the mouse.
False
5
inv-proof
[(((((triple4 ((triple10) -> rule9)) -> rule8)) -> rule2))]
("bear" "needs" "mouse" "-")
((((triple4 ((triple10) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cat is rough.
True
8
proof
[(((((((((triple10) -> rule4)) -> rule1) triple10) -> rule7) ((triple10) -> rule9)) -> rule8))]
("cat" "is" "rough" "+")
((((((((triple10) -> (rule4 % int5))) -> (rule1 % int4)) triple10) -> (rule7 % int3)) ((triple10) -> (rule9 % int2))) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int3
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int4
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int5
The mouse does not see the bear.
False
7
inv-proof
[(((((((triple8 ((triple10) -> rule9)) -> rule8)) -> rule2) triple7) -> rule3))]
("mouse" "sees" "bear" "-")
((((((triple8 ((triple10) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) triple7) -> (rule3 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4
The cat needs the mouse.
True
9
proof
[(((((((((((triple10) -> rule4)) -> rule1) triple10) -> rule7) ((triple10) -> rule9)) -> rule8)) -> rule2))]
("cat" "needs" "mouse" "+")
((((((((((triple10) -> (rule4 % int6))) -> (rule1 % int5)) triple10) -> (rule7 % int4)) ((triple10) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int4
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int5
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int6
The cat does not need the mouse.
False
9
inv-proof
[(((((((((((triple10) -> rule4)) -> rule1) triple10) -> rule7) ((triple10) -> rule9)) -> rule8)) -> rule2))]
("cat" "needs" "mouse" "-")
((((((((((triple10) -> (rule4 % int6))) -> (rule1 % int5)) triple10) -> (rule7 % int4)) ((triple10) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int4
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int5
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int6
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("bear" "is" "young" "-")
The cat sees the cow.
Unknown
rconc
[@1: The cat sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "sees" "cow" "+")
The bear does not see the cow.
Unknown
inv-rconc
[@1: The bear sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "sees" "cow" "-")
The mouse is rough.
Unknown
rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "is" "rough" "+")
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cat" "is" "young" "-")
The cow visits the cat.
Unknown
rconc
[@2: The cow visits the cat.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("cow" "visits" "cat" "+")
The bear does not need the cow.
Unknown
inv-random
[@0: The bear needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cow" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cat needs the bear.
Unknown
random
[@0: The cat needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "bear" "+")
The cow does not see the mouse.
Unknown
inv-random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear is nice.[(triple1)] The bear sees the cat.[(triple2)] The bear visits the cat.[(triple3)] The bear visits the mouse.[(triple4)] The cat is nice.[(triple5)] The cat sees the bear.[(triple6)] The cow needs the bear.[(triple7)] The cow visits the mouse.[(triple8)] The mouse sees the cat.[(triple9)] The mouse visits the bear.[(triple10)] @1: The mouse is young.[(((triple10) -> rule9))] The mouse needs the bear.[(((triple8 triple7) -> rule6))] The mouse sees the cow.[(((triple10) -> rule4))] @2: The bear is rough.[(((triple4 ((triple10) -> rule9)) -> rule8))] The cow is rough.[(((triple8 ((triple10) -> rule9)) -> rule8))] The mouse visits the cat.[(((((triple10) -> rule4)) -> rule1))] @3: The bear needs the mouse.[(((((triple4 ((triple10) -> rule9)) -> rule8)) -> rule2))] The cat visits the mouse.[(((((((triple10) -> rule4)) -> rule1) triple10) -> rule7))] The cow needs the mouse.[(((((triple8 ((triple10) -> rule9)) -> rule8)) -> rule2))] @4: The cat is rough.[(((((((((triple10) -> rule4)) -> rule1) triple10) -> rule7) ((triple10) -> rule9)) -> rule8))] The mouse sees the bear.[(((((((triple8 ((triple10) -> rule9)) -> rule8)) -> rule2) triple7) -> rule3))] @5: The cat needs the mouse.[(((((((((((triple10) -> rule4)) -> rule1) triple10) -> rule7) ((triple10) -> rule9)) -> rule8)) -> rule2))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear sees the cat.
("bear" "sees" "cat" "+")
triple2
The bear visits the cat.
("bear" "visits" "cat" "+")
triple3
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat sees the bear.
("cat" "sees" "bear" "+")
triple6
The cow needs the bear.
("cow" "needs" "bear" "+")
triple7
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple8
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple9
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple10
The mouse is young.
("mouse" "is" "young" "+")
((triple10) -> (rule9 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple8 triple7) -> (rule6 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((triple10) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
((triple4 ((triple10) -> (rule9 % int2))) -> (rule8 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
((triple8 ((triple10) -> (rule9 % int2))) -> (rule8 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
((((triple10) -> (rule4 % int2))) -> (rule1 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((((triple4 ((triple10) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((((((triple10) -> (rule4 % int3))) -> (rule1 % int2)) triple10) -> (rule7 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((((triple8 ((triple10) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
((((((((triple10) -> (rule4 % int5))) -> (rule1 % int4)) triple10) -> (rule7 % int3)) ((triple10) -> (rule9 % int2))) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int3
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int4
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int5
The mouse sees the bear.
("mouse" "sees" "bear" "+")
((((((triple8 ((triple10) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) triple7) -> (rule3 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((((((((((triple10) -> (rule4 % int6))) -> (rule1 % int5)) triple10) -> (rule7 % int4)) ((triple10) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int4
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int5
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int6