The mouse eats the tiger. The mouse is big. The mouse is nice. The mouse likes the tiger. The mouse sees the tiger. The tiger eats the mouse. The tiger is big. If the mouse is big then the mouse eats the tiger. If something is cold then it sees the tiger. If something is nice and it sees the mouse then it sees the tiger. If the mouse eats the tiger then the tiger is nice. If the tiger eats the mouse then the mouse eats the tiger. If something is nice then it is cold. If something eats the mouse then it is round. If the mouse is big and the mouse is nice then the mouse sees the tiger.
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
If the mouse is big then the mouse eats the tiger.
((("mouse" "is" "big" "+")) -> ("mouse" "eats" "tiger" "+"))
If something is cold then it sees the tiger.
((("something" "is" "cold" "+")) -> ("something" "sees" "tiger" "+"))
If something is nice and it sees the mouse then it sees the tiger.
((("something" "is" "nice" "+") ("something" "sees" "mouse" "+")) -> ("something" "sees" "tiger" "+"))
If the mouse eats the tiger then the tiger is nice.
((("mouse" "eats" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
If the tiger eats the mouse then the mouse eats the tiger.
((("tiger" "eats" "mouse" "+")) -> ("mouse" "eats" "tiger" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something eats the mouse then it is round.
((("something" "eats" "mouse" "+")) -> ("something" "is" "round" "+"))
If the mouse is big and the mouse is nice then the mouse sees the tiger.
((("mouse" "is" "big" "+") ("mouse" "is" "nice" "+")) -> ("mouse" "sees" "tiger" "+"))
The mouse is nice.
True
1
proof
[(triple3)]
("mouse" "is" "nice" "+")
triple3
The mouse is not big.
False
1
inv-proof
[(triple2)]
("mouse" "is" "big" "-")
triple2
The tiger is round.
True
2
proof
[(((triple6) -> rule7))]
("tiger" "is" "round" "+")
((triple6) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is not round.
False
2
inv-proof
[(((triple6) -> rule7))]
("tiger" "is" "round" "-")
((triple6) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is cold.
True
3
proof
[(((((triple1) -> rule4)) -> rule6) OR ((((((triple2) -> rule1)) -> rule4)) -> rule6) OR ((((((triple6) -> rule5)) -> rule4)) -> rule6))]
("tiger" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The tiger is not cold.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6) OR ((((((triple2) -> rule1)) -> rule4)) -> rule6) OR ((((((triple6) -> rule5)) -> rule4)) -> rule6))]
("tiger" "is" "cold" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The tiger sees the tiger.
True
4
proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule2) OR ((((((((triple2) -> rule1)) -> rule4)) -> rule6)) -> rule2) OR ((((((((triple6) -> rule5)) -> rule4)) -> rule6)) -> rule2))]
("tiger" "sees" "tiger" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int4
The tiger does not see the tiger.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule2) OR ((((((((triple2) -> rule1)) -> rule4)) -> rule6)) -> rule2) OR ((((((((triple6) -> rule5)) -> rule4)) -> rule6)) -> rule2))]
("tiger" "sees" "tiger" "-")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int4
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "round" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
The tiger does not see the mouse.
Unknown
inv-random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "mouse" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The tiger does not like the mouse.
Unknown
inv-random
[@0: The tiger likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "mouse" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The mouse eats the tiger.[(triple1 OR ((triple2) -> rule1) OR ((triple6) -> rule5))] The mouse is big.[(triple2)] The mouse is nice.[(triple3)] The mouse likes the tiger.[(triple4)] The mouse sees the tiger.[(triple5 OR ((triple2 triple3) -> rule8) OR ((((triple3) -> rule6)) -> rule2))] The tiger eats the mouse.[(triple6)] The tiger is big.[(triple7)] @1: The mouse is cold.[(((triple3) -> rule6))] The tiger is nice.[(((triple1) -> rule4) OR ((((triple2) -> rule1)) -> rule4) OR ((((triple6) -> rule5)) -> rule4))] The tiger is round.[(((triple6) -> rule7))] @2: The tiger is cold.[(((((triple1) -> rule4)) -> rule6) OR ((((((triple2) -> rule1)) -> rule4)) -> rule6) OR ((((((triple6) -> rule5)) -> rule4)) -> rule6))] @3: The tiger sees the tiger.[(((((((triple1) -> rule4)) -> rule6)) -> rule2) OR ((((((((triple2) -> rule1)) -> rule4)) -> rule6)) -> rule2) OR ((((((((triple6) -> rule5)) -> rule4)) -> rule6)) -> rule2))]
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple1
((triple2) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
((triple6) -> (rule5 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple4
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple5
((triple2 triple3) -> (rule8 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
((triple3) -> (rule6 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
((triple6) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int4