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