The bear chases the mouse. The cat chases the mouse. The lion is kind. The mouse is rough. If someone chases the cat then the cat likes the bear. If the mouse is kind and the mouse likes the cat then the cat chases the mouse. If someone is blue and they like the mouse then the mouse chases the lion. If someone eats the mouse then they eat the cat. If someone chases the bear then the bear likes the cat. If someone is nice then they chase the bear. If someone chases the mouse then they chase the cat. If someone chases the cat and the cat likes the bear then the bear eats the cat.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The lion is kind.
("lion" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
If someone chases the cat then the cat likes the bear.
((("someone" "chases" "cat" "+")) -> ("cat" "likes" "bear" "+"))
If the mouse is kind and the mouse likes the cat then the cat chases the mouse.
((("mouse" "is" "kind" "+") ("mouse" "likes" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If someone is blue and they like the mouse then the mouse chases the lion.
((("someone" "is" "blue" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "chases" "lion" "+"))
If someone eats the mouse then they eat the cat.
((("someone" "eats" "mouse" "+")) -> ("someone" "eats" "cat" "+"))
If someone chases the bear then the bear likes the cat.
((("someone" "chases" "bear" "+")) -> ("bear" "likes" "cat" "+"))
If someone is nice then they chase the bear.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the mouse then they chase the cat.
((("someone" "chases" "mouse" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the cat and the cat likes the bear then the bear eats the cat.
((("someone" "chases" "cat" "+") ("cat" "likes" "bear" "+")) -> ("bear" "eats" "cat" "+"))
The cat chases the mouse.
True
1
proof
[(triple2)]
("cat" "chases" "mouse" "+")
triple2
The mouse is not rough.
False
1
inv-proof
[(triple4)]
("mouse" "is" "rough" "-")
triple4
The cat chases the cat.
True
2
proof
[(((triple2) -> rule7))]
("cat" "chases" "cat" "+")
((triple2) -> (rule7 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The bear does not chase the cat.
False
2
inv-proof
[(((triple1) -> rule7))]
("bear" "chases" "cat" "-")
((triple1) -> (rule7 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The cat likes the bear.
True
3
proof
[(((((triple1) -> rule7)) -> rule1) OR ((((triple2) -> rule7)) -> rule1))]
("cat" "likes" "bear" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat does not like the bear.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule1) OR ((((triple2) -> rule7)) -> rule1))]
("cat" "likes" "bear" "-")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The bear eats the cat.
True
6
proof
[(((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule1)) -> rule8) OR ((((triple1) -> rule7) ((((triple2) -> rule7)) -> rule1)) -> rule8) OR ((((triple2) -> rule7) ((((triple1) -> rule7)) -> rule1)) -> rule8) OR ((((triple2) -> rule7) ((((triple2) -> rule7)) -> rule1)) -> rule8))]
("bear" "eats" "cat" "+")
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear chases the cat.
("bear" "chases" "cat" "+")
int3
((((triple1) -> (rule7 % int4)) ((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The bear chases the cat.
("bear" "chases" "cat" "+")
int4
((((triple2) -> (rule7 % int4)) ((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear chases the cat.
("bear" "chases" "cat" "+")
int3
The cat chases the cat.
("cat" "chases" "cat" "+")
int4
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The bear does not eat the cat.
False
6
inv-proof
[(((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule1)) -> rule8) OR ((((triple1) -> rule7) ((((triple2) -> rule7)) -> rule1)) -> rule8) OR ((((triple2) -> rule7) ((((triple1) -> rule7)) -> rule1)) -> rule8) OR ((((triple2) -> rule7) ((((triple2) -> rule7)) -> rule1)) -> rule8))]
("bear" "eats" "cat" "-")
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear chases the cat.
("bear" "chases" "cat" "+")
int3
((((triple1) -> (rule7 % int4)) ((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The bear chases the cat.
("bear" "chases" "cat" "+")
int4
((((triple2) -> (rule7 % int4)) ((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear chases the cat.
("bear" "chases" "cat" "+")
int3
The cat chases the cat.
("cat" "chases" "cat" "+")
int4
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The mouse does not eat the cat.
Unknown
inv-rconc
[@1: The mouse eats the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "eats" "cat" "-")
The bear likes the cat.
Unknown
rconc
[@2: The bear likes the cat.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("bear" "likes" "cat" "+")
The lion does not chase the bear.
Unknown
inv-rconc
[@1: The lion chases the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "chases" "bear" "-")
The lion eats the cat.
Unknown
rconc
[@1: The lion eats the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "eats" "cat" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The mouse likes the bear.
Unknown
random
[@0: The mouse likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "bear" "+")
The mouse does not eat the bear.
Unknown
inv-random
[@0: The mouse eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "bear" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The bear chases the mouse.[(triple1)] The cat chases the mouse.[(triple2)] The lion is kind.[(triple3)] The mouse is rough.[(triple4)] @1: The bear chases the cat.[(((triple1) -> rule7))] The cat chases the cat.[(((triple2) -> rule7))] @2: The cat likes the bear.[(((((triple1) -> rule7)) -> rule1) OR ((((triple2) -> rule7)) -> rule1))] @3: The bear eats the cat.[(((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule1)) -> rule8) OR ((((triple1) -> rule7) ((((triple2) -> rule7)) -> rule1)) -> rule8) OR ((((triple2) -> rule7) ((((triple1) -> rule7)) -> rule1)) -> rule8) OR ((((triple2) -> rule7) ((((triple2) -> rule7)) -> rule1)) -> rule8))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The bear chases the cat.
("bear" "chases" "cat" "+")
((triple1) -> (rule7 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple2) -> (rule7 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The bear eats the cat.
("bear" "eats" "cat" "+")
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear chases the cat.
("bear" "chases" "cat" "+")
int3
((((triple1) -> (rule7 % int4)) ((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The bear chases the cat.
("bear" "chases" "cat" "+")
int4
((((triple2) -> (rule7 % int4)) ((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear chases the cat.
("bear" "chases" "cat" "+")
int3
The cat chases the cat.
("cat" "chases" "cat" "+")
int4
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3