The cat chases the mouse. The cat eats the mouse. The cat is big. The cat is rough. The cat sees the mouse. The mouse chases the cat. The mouse chases the tiger. The mouse eats the tiger. The mouse is big. The mouse is blue. The mouse is cold. The mouse is rough. The mouse sees the cat. The mouse sees the tiger. The tiger eats the mouse. The tiger is rough. If the tiger sees the mouse then the mouse sees the cat. If someone chases the mouse then the mouse sees the cat. If someone eats the mouse then they are cold. If someone eats the mouse and the mouse sees the cat then they eat the cat. If someone chases the mouse then they see the cat. If someone chases the cat then the cat is round. If the tiger is big then the tiger eats the mouse. If someone sees the cat and the cat is round then they eat the mouse.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If the tiger sees the mouse then the mouse sees the cat.
((("tiger" "sees" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
If someone chases the mouse then the mouse sees the cat.
((("someone" "chases" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
If someone eats the mouse then they are cold.
((("someone" "eats" "mouse" "+")) -> ("someone" "is" "cold" "+"))
If someone eats the mouse and the mouse sees the cat then they eat the cat.
((("someone" "eats" "mouse" "+") ("mouse" "sees" "cat" "+")) -> ("someone" "eats" "cat" "+"))
If someone chases the mouse then they see the cat.
((("someone" "chases" "mouse" "+")) -> ("someone" "sees" "cat" "+"))
If someone chases the cat then the cat is round.
((("someone" "chases" "cat" "+")) -> ("cat" "is" "round" "+"))
If the tiger is big then the tiger eats the mouse.
((("tiger" "is" "big" "+")) -> ("tiger" "eats" "mouse" "+"))
If someone sees the cat and the cat is round then they eat the mouse.
((("someone" "sees" "cat" "+") ("cat" "is" "round" "+")) -> ("someone" "eats" "mouse" "+"))
The cat is big.
True
1
proof
[(triple3)]
("cat" "is" "big" "+")
triple3
The mouse does not see the tiger.
False
1
inv-proof
[(triple14)]
("mouse" "sees" "tiger" "-")
triple14
The tiger eats the cat.
True
3
proof
[(((triple15 triple13) -> rule4) OR ((triple15 ((triple1) -> rule2)) -> rule4))]
("tiger" "eats" "cat" "+")
((triple15 triple13) -> (rule4 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
((triple15 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The tiger does not eat the cat.
False
3
inv-proof
[(((triple15 triple13) -> rule4) OR ((triple15 ((triple1) -> rule2)) -> rule4))]
("tiger" "eats" "cat" "-")
((triple15 triple13) -> (rule4 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
((triple15 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse eats the mouse.
True
4
proof
[(((triple13 ((triple6) -> rule6)) -> rule8) OR ((((triple1) -> rule2) ((triple6) -> rule6)) -> rule8))]
("mouse" "eats" "mouse" "+")
((triple13 ((triple6) -> (rule6 % int2))) -> (rule8 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple6) -> (rule6 % int2))) -> (rule8 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The mouse does not eat the mouse.
False
4
inv-proof
[(((triple13 ((triple6) -> rule6)) -> rule8) OR ((((triple1) -> rule2) ((triple6) -> rule6)) -> rule8))]
("mouse" "eats" "mouse" "-")
((triple13 ((triple6) -> (rule6 % int2))) -> (rule8 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple6) -> (rule6 % int2))) -> (rule8 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The mouse eats the cat.
True
6
proof
[(((((triple13 ((triple6) -> rule6)) -> rule8) triple13) -> rule4) OR ((((triple13 ((triple6) -> rule6)) -> rule8) ((triple1) -> rule2)) -> rule4) OR ((((((triple1) -> rule2) ((triple6) -> rule6)) -> rule8) triple13) -> rule4) OR ((((((triple1) -> rule2) ((triple6) -> rule6)) -> rule8) ((triple1) -> rule2)) -> rule4))]
("mouse" "eats" "cat" "+")
((((triple13 ((triple6) -> (rule6 % int3))) -> (rule8 % int2)) triple13) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple13 ((triple6) -> (rule6 % int4))) -> (rule8 % int3)) ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
((((((triple1) -> (rule2 % int4)) ((triple6) -> (rule6 % int3))) -> (rule8 % int2)) triple13) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
((((((triple1) -> (rule2 % int4)) ((triple6) -> (rule6 % int3))) -> (rule8 % int2)) ((triple1) -> (rule2 % int4))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
The mouse does not eat the cat.
False
6
inv-proof
[(((((triple13 ((triple6) -> rule6)) -> rule8) triple13) -> rule4) OR ((((triple13 ((triple6) -> rule6)) -> rule8) ((triple1) -> rule2)) -> rule4) OR ((((((triple1) -> rule2) ((triple6) -> rule6)) -> rule8) triple13) -> rule4) OR ((((((triple1) -> rule2) ((triple6) -> rule6)) -> rule8) ((triple1) -> rule2)) -> rule4))]
("mouse" "eats" "cat" "-")
((((triple13 ((triple6) -> (rule6 % int3))) -> (rule8 % int2)) triple13) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple13 ((triple6) -> (rule6 % int4))) -> (rule8 % int3)) ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
((((((triple1) -> (rule2 % int4)) ((triple6) -> (rule6 % int3))) -> (rule8 % int2)) triple13) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
((((((triple1) -> (rule2 % int4)) ((triple6) -> (rule6 % int3))) -> (rule8 % int2)) ((triple1) -> (rule2 % int4))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
The tiger does not see the cat.
Unknown
inv-rconc
[@1: The tiger sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "sees" "cat" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The cat eats the tiger.
Unknown
random
[@0: The cat eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "tiger" "+")
The tiger does not chase the cat.
Unknown
inv-random
[@0: The tiger chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cat" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
@0: The cat chases the mouse.[(triple1)] The cat eats the mouse.[(triple2 OR ((((triple1) -> rule5) ((triple6) -> rule6)) -> rule8))] The cat is big.[(triple3)] The cat is rough.[(triple4)] The cat sees the mouse.[(triple5)] The mouse chases the cat.[(triple6)] The mouse chases the tiger.[(triple7)] The mouse eats the tiger.[(triple8)] The mouse is big.[(triple9)] The mouse is blue.[(triple10)] The mouse is cold.[(triple11 OR ((((triple13 ((triple6) -> rule6)) -> rule8)) -> rule3) OR ((((((triple1) -> rule2) ((triple6) -> rule6)) -> rule8)) -> rule3))] The mouse is rough.[(triple12)] The mouse sees the cat.[(triple13 OR ((triple1) -> rule2))] The mouse sees the tiger.[(triple14)] The tiger eats the mouse.[(triple15)] The tiger is rough.[(triple16)] @1: The cat eats the cat.[(((triple2 triple13) -> rule4) OR ((triple2 ((triple1) -> rule2)) -> rule4) OR ((((((triple1) -> rule5) ((triple6) -> rule6)) -> rule8) triple13) -> rule4) OR ((((((triple1) -> rule5) ((triple6) -> rule6)) -> rule8) ((triple1) -> rule2)) -> rule4))] The cat is cold.[(((triple2) -> rule3) OR ((((((triple1) -> rule5) ((triple6) -> rule6)) -> rule8)) -> rule3))] The cat is round.[(((triple6) -> rule6))] The cat sees the cat.[(((triple1) -> rule5))] The tiger eats the cat.[(((triple15 triple13) -> rule4) OR ((triple15 ((triple1) -> rule2)) -> rule4))] The tiger is cold.[(((triple15) -> rule3))] @2: The mouse eats the mouse.[(((triple13 ((triple6) -> rule6)) -> rule8) OR ((((triple1) -> rule2) ((triple6) -> rule6)) -> rule8))] @3: The mouse eats the cat.[(((((triple13 ((triple6) -> rule6)) -> rule8) triple13) -> rule4) OR ((((triple13 ((triple6) -> rule6)) -> rule8) ((triple1) -> rule2)) -> rule4) OR ((((((triple1) -> rule2) ((triple6) -> rule6)) -> rule8) triple13) -> rule4) OR ((((((triple1) -> rule2) ((triple6) -> rule6)) -> rule8) ((triple1) -> rule2)) -> rule4))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
((((triple1) -> (rule5 % int3)) ((triple6) -> (rule6 % int2))) -> (rule8 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
int3
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple6
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple7
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple8
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
((((triple13 ((triple6) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple1) -> (rule2 % int4)) ((triple6) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
The mouse is rough.
("mouse" "is" "rough" "+")
triple12
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple13
((triple1) -> (rule2 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple14
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple15
The tiger is rough.
("tiger" "is" "rough" "+")
triple16
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple2 triple13) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
((triple2 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
((((((triple1) -> (rule5 % int4)) ((triple6) -> (rule6 % int3))) -> (rule8 % int2)) triple13) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat sees the cat.
("cat" "sees" "cat" "+")
int4
((((((triple1) -> (rule5 % int5)) ((triple6) -> (rule6 % int4))) -> (rule8 % int3)) ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
The cat sees the cat.
("cat" "sees" "cat" "+")
int5
The cat is cold.
("cat" "is" "cold" "+")
((triple2) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((((((triple1) -> (rule5 % int4)) ((triple6) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat sees the cat.
("cat" "sees" "cat" "+")
int4
The cat is round.
("cat" "is" "round" "+")
((triple6) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple1) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
((triple15 triple13) -> (rule4 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
((triple15 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
((triple15) -> (rule3 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple13 ((triple6) -> (rule6 % int2))) -> (rule8 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple6) -> (rule6 % int2))) -> (rule8 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The mouse eats the cat.
("mouse" "eats" "cat" "+")
((((triple13 ((triple6) -> (rule6 % int3))) -> (rule8 % int2)) triple13) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple13 ((triple6) -> (rule6 % int4))) -> (rule8 % int3)) ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
((((((triple1) -> (rule2 % int4)) ((triple6) -> (rule6 % int3))) -> (rule8 % int2)) triple13) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4
((((((triple1) -> (rule2 % int4)) ((triple6) -> (rule6 % int3))) -> (rule8 % int2)) ((triple1) -> (rule2 % int4))) -> (rule4 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4