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