The mouse eats the tiger. The mouse is kind. The mouse visits the tiger. The tiger eats the mouse. The tiger is blue. The tiger is kind. The tiger visits the mouse. If something visits the tiger then it visits the mouse. If something visits the mouse then it is blue. If something is blue then it is green.
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something visits the tiger then it visits the mouse.
((("something" "visits" "tiger" "+")) -> ("something" "visits" "mouse" "+"))
If something visits the mouse then it is blue.
((("something" "visits" "mouse" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
The tiger eats the mouse.
True
1
proof
[(triple4)]
("tiger" "eats" "mouse" "+")
triple4
The tiger does not visit the mouse.
False
1
inv-proof
[(triple7)]
("tiger" "visits" "mouse" "-")
triple7
The tiger is green.
True
2
proof
[(((triple5) -> rule3) OR ((((triple7) -> rule2)) -> rule3))]
("tiger" "is" "green" "+")
((triple5) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The mouse does not visit the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("mouse" "visits" "mouse" "-")
((triple3) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is blue.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("mouse" "is" "blue" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is not blue.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("mouse" "is" "blue" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is green.
True
4
proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("mouse" "is" "green" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The mouse is not green.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("mouse" "is" "green" "-")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The mouse chases the tiger.
Unknown
random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "+")
@0: The mouse eats the tiger.[(triple1)] The mouse is kind.[(triple2)] The mouse visits the tiger.[(triple3)] The tiger eats the mouse.[(triple4)] The tiger is blue.[(triple5 OR ((triple7) -> rule2))] The tiger is kind.[(triple6)] The tiger visits the mouse.[(triple7)] @1: The mouse visits the mouse.[(((triple3) -> rule1))] The tiger is green.[(((triple5) -> rule3) OR ((((triple7) -> rule2)) -> rule3))] @2: The mouse is blue.[(((((triple3) -> rule1)) -> rule2))] @3: The mouse is green.[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple3
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple4
The tiger is blue.
("tiger" "is" "blue" "+")
triple5
((triple7) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple3) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple5) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3