The cat is red. The cat is rough. The cat needs the tiger. The cat sees the tiger. The mouse is green. The mouse needs the tiger. The mouse sees the cat. The mouse sees the tiger. The tiger eats the mouse. The tiger sees the cat. If someone is cold then they eat the tiger. If someone sees the mouse and the mouse eats the tiger then the tiger needs the mouse. If someone eats the mouse then the mouse sees the tiger. If someone eats the tiger then the tiger sees the mouse. If someone eats the mouse then the mouse eats the tiger. If the mouse is red then the mouse is cold. If someone eats the mouse and the mouse eats the tiger then the mouse is red. If the mouse sees the tiger and the tiger eats the mouse then the mouse is cold.
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
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 sees the cat.
("tiger" "sees" "cat" "+")
If someone is cold then they eat the tiger.
((("someone" "is" "cold" "+")) -> ("someone" "eats" "tiger" "+"))
If someone sees the mouse and the mouse eats the tiger then the tiger needs the mouse.
((("someone" "sees" "mouse" "+") ("mouse" "eats" "tiger" "+")) -> ("tiger" "needs" "mouse" "+"))
If someone eats the mouse then the mouse sees the tiger.
((("someone" "eats" "mouse" "+")) -> ("mouse" "sees" "tiger" "+"))
If someone eats the tiger then the tiger sees the mouse.
((("someone" "eats" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
If someone eats the mouse then the mouse eats the tiger.
((("someone" "eats" "mouse" "+")) -> ("mouse" "eats" "tiger" "+"))
If the mouse is red then the mouse is cold.
((("mouse" "is" "red" "+")) -> ("mouse" "is" "cold" "+"))
If someone eats the mouse and the mouse eats the tiger then the mouse is red.
((("someone" "eats" "mouse" "+") ("mouse" "eats" "tiger" "+")) -> ("mouse" "is" "red" "+"))
If the mouse sees the tiger and the tiger eats the mouse then the mouse is cold.
((("mouse" "sees" "tiger" "+") ("tiger" "eats" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
The cat sees the tiger.
True
1
proof
[(triple4)]
("cat" "sees" "tiger" "+")
triple4
The mouse does not see the tiger.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule3))]
("mouse" "sees" "tiger" "-")
triple8
((triple9) -> (rule3 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse eats the tiger.
True
2
proof
[(((triple9) -> rule5) OR ((((triple8 triple9) -> rule8)) -> rule1) OR ((((((triple9) -> rule3) triple9) -> rule8)) -> rule1))]
("mouse" "eats" "tiger" "+")
((triple9) -> (rule5 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
((((triple8 triple9) -> (rule8 % int2))) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((((((triple9) -> (rule3 % int3)) triple9) -> (rule8 % int2))) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The mouse does not eat the tiger.
False
2
inv-proof
[(((triple9) -> rule5) OR ((((triple8 triple9) -> rule8)) -> rule1) OR ((((((triple9) -> rule3) triple9) -> rule8)) -> rule1))]
("mouse" "eats" "tiger" "-")
((triple9) -> (rule5 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
((((triple8 triple9) -> (rule8 % int2))) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((((((triple9) -> (rule3 % int3)) triple9) -> (rule8 % int2))) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The mouse is red.
True
4
proof
[(((triple9 ((triple9) -> rule5)) -> rule7) OR ((triple9 ((((triple8 triple9) -> rule8)) -> rule1)) -> rule7) OR ((triple9 ((((((triple9) -> rule3) triple9) -> rule8)) -> rule1)) -> rule7))]
("mouse" "is" "red" "+")
((triple9 ((triple9) -> (rule5 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
((triple9 ((((triple8 triple9) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((triple9 ((((((triple9) -> (rule3 % int4)) triple9) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The tiger does not see the mouse.
False
3
inv-proof
[(((((triple9) -> rule5)) -> rule4) OR ((((((triple8 triple9) -> rule8)) -> rule1)) -> rule4) OR ((((((((triple9) -> rule3) triple9) -> rule8)) -> rule1)) -> rule4))]
("tiger" "sees" "mouse" "-")
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
((((((triple8 triple9) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((((((((triple9) -> (rule3 % int4)) triple9) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The cat does not eat the tiger.
Unknown
inv-rconc
[@1: The cat eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "tiger" "-")
The tiger eats the tiger.
Unknown
rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The mouse does not need the cat.
Unknown
inv-random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The cat is red.[(triple1)] The cat is rough.[(triple2)] The cat needs the tiger.[(triple3)] The cat sees the tiger.[(triple4)] The mouse is green.[(triple5)] The mouse needs the tiger.[(triple6)] The mouse sees the cat.[(triple7)] The mouse sees the tiger.[(triple8 OR ((triple9) -> rule3))] The tiger eats the mouse.[(triple9)] The tiger sees the cat.[(triple10)] @1: The mouse eats the tiger.[(((triple9) -> rule5) OR ((((triple8 triple9) -> rule8)) -> rule1) OR ((((((triple9) -> rule3) triple9) -> rule8)) -> rule1))] The mouse is cold.[(((triple8 triple9) -> rule8) OR ((((triple9) -> rule3) triple9) -> rule8) OR ((((triple9 ((triple9) -> rule5)) -> rule7)) -> rule6))] @2: The mouse is red.[(((triple9 ((triple9) -> rule5)) -> rule7) OR ((triple9 ((((triple8 triple9) -> rule8)) -> rule1)) -> rule7) OR ((triple9 ((((((triple9) -> rule3) triple9) -> rule8)) -> rule1)) -> rule7))] The tiger sees the mouse.[(((((triple9) -> rule5)) -> rule4) OR ((((((triple8 triple9) -> rule8)) -> rule1)) -> rule4) OR ((((((((triple9) -> rule3) triple9) -> rule8)) -> rule1)) -> rule4))] @3: The tiger needs the mouse.[(((((((triple9) -> rule5)) -> rule4) ((triple9) -> rule5)) -> rule2) OR ((((((triple9) -> rule5)) -> rule4) ((((triple8 triple9) -> rule8)) -> rule1)) -> rule2) OR ((((((((triple8 triple9) -> rule8)) -> rule1)) -> rule4) ((triple9) -> rule5)) -> rule2) OR ((((((triple9) -> rule5)) -> rule4) ((((((triple9) -> rule3) triple9) -> rule8)) -> rule1)) -> rule2) OR ((((((((triple8 triple9) -> rule8)) -> rule1)) -> rule4) ((((triple8 triple9) -> rule8)) -> rule1)) -> rule2) OR ((((((((triple8 triple9) -> rule8)) -> rule1)) -> rule4) ((((((triple9) -> rule3) triple9) -> rule8)) -> rule1)) -> rule2) OR ((((((((((triple9) -> rule3) triple9) -> rule8)) -> rule1)) -> rule4) ((triple9) -> rule5)) -> rule2) OR ((((((((((triple9) -> rule3) triple9) -> rule8)) -> rule1)) -> rule4) ((((triple8 triple9) -> rule8)) -> rule1)) -> rule2) OR ((((((((((triple9) -> rule3) triple9) -> rule8)) -> rule1)) -> rule4) ((((((triple9) -> rule3) triple9) -> rule8)) -> rule1)) -> rule2))]
The cat is red.
("cat" "is" "red" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple4
The mouse is green.
("mouse" "is" "green" "+")
triple5
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple6
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple7
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple8
((triple9) -> (rule3 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple9
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple10
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((triple9) -> (rule5 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
((((triple8 triple9) -> (rule8 % int2))) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((((((triple9) -> (rule3 % int3)) triple9) -> (rule8 % int2))) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
((triple8 triple9) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((((triple9) -> (rule3 % int2)) triple9) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
((((triple9 ((triple9) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
((triple9 ((triple9) -> (rule5 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
((triple9 ((((triple8 triple9) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((triple9 ((((((triple9) -> (rule3 % int4)) triple9) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
((((((triple8 triple9) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((((((((triple9) -> (rule3 % int4)) triple9) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
((((((triple9) -> (rule5 % int3))) -> (rule4 % int2)) ((triple9) -> (rule5 % int3))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
((((((triple9) -> (rule5 % int4))) -> (rule4 % int3)) ((((triple8 triple9) -> (rule8 % int2))) -> (rule1 % int4))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int4
((((((((triple8 triple9) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((triple9) -> (rule5 % int3))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
int4
((((((triple9) -> (rule5 % int5))) -> (rule4 % int4)) ((((((triple9) -> (rule3 % int3)) triple9) -> (rule8 % int2))) -> (rule1 % int5))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int4
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int5
((((((((triple8 triple9) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((triple8 triple9) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
int4
((((((((triple8 triple9) -> (rule8 % int5))) -> (rule1 % int4))) -> (rule4 % int3)) ((((((triple9) -> (rule3 % int2)) triple9) -> (rule8 % int5))) -> (rule1 % int4))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int4
The mouse is cold.
("mouse" "is" "cold" "+")
int5
((((((((((triple9) -> (rule3 % int5)) triple9) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((triple9) -> (rule5 % int3))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
int4
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int5
((((((((((triple9) -> (rule3 % int5)) triple9) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((triple8 triple9) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
int4
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int5
((((((((((triple9) -> (rule3 % int5)) triple9) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((((triple9) -> (rule3 % int5)) triple9) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
int4
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int5