The mouse chases the tiger. The mouse eats the tiger. The mouse is blue. The mouse is cold. The mouse is kind. The mouse is rough. The mouse visits the tiger. The tiger chases the mouse. The tiger eats the mouse. The tiger is blue. The tiger is cold. The tiger is kind. The tiger is rough. The tiger is young. The tiger visits the mouse. If something visits the mouse and the mouse chases the tiger then the tiger visits the mouse. If something visits the mouse then it is cold. If the mouse visits the tiger then the mouse is kind. If something is rough then it visits the mouse. If something is kind then it is young. If something is cold then it visits the tiger.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something visits the mouse and the mouse chases the tiger then the tiger visits the mouse.
((("something" "visits" "mouse" "+") ("mouse" "chases" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If something visits the mouse then it is cold.
((("something" "visits" "mouse" "+")) -> ("something" "is" "cold" "+"))
If the mouse visits the tiger then the mouse is kind.
((("mouse" "visits" "tiger" "+")) -> ("mouse" "is" "kind" "+"))
If something is rough then it visits the mouse.
((("something" "is" "rough" "+")) -> ("something" "visits" "mouse" "+"))
If something is kind then it is young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is cold then it visits the tiger.
((("something" "is" "cold" "+")) -> ("something" "visits" "tiger" "+"))
The tiger is cold.
True
1
proof
[(triple11 OR ((triple15) -> rule2) OR ((((triple13) -> rule4)) -> rule2) OR ((((((triple6) -> rule4) triple1) -> rule1)) -> rule2))]
("tiger" "is" "cold" "+")
triple11
((triple15) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
((((((triple6) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The mouse is not blue.
False
1
inv-proof
[(triple3)]
("mouse" "is" "blue" "-")
triple3
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 tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The mouse chases the tiger.[(triple1)] The mouse eats the tiger.[(triple2)] The mouse is blue.[(triple3)] The mouse is cold.[(triple4 OR ((((triple6) -> rule4)) -> rule2))] The mouse is kind.[(triple5 OR ((triple7) -> rule3) OR ((((triple4) -> rule6)) -> rule3) OR ((((((((triple6) -> rule4)) -> rule2)) -> rule6)) -> rule3))] The mouse is rough.[(triple6)] The mouse visits the tiger.[(triple7 OR ((triple4) -> rule6) OR ((((((triple6) -> rule4)) -> rule2)) -> rule6))] The tiger chases the mouse.[(triple8)] The tiger eats the mouse.[(triple9)] The tiger is blue.[(triple10)] The tiger is cold.[(triple11 OR ((triple15) -> rule2) OR ((((triple13) -> rule4)) -> rule2) OR ((((((triple6) -> rule4) triple1) -> rule1)) -> rule2))] The tiger is kind.[(triple12)] The tiger is rough.[(triple13)] The tiger is young.[(triple14 OR ((triple12) -> rule5))] The tiger visits the mouse.[(triple15 OR ((triple13) -> rule4) OR ((((triple6) -> rule4) triple1) -> rule1))] @1: The mouse is young.[(((triple5) -> rule5) OR ((((triple7) -> rule3)) -> rule5) OR ((((((triple4) -> rule6)) -> rule3)) -> rule5) OR ((((((((((triple6) -> rule4)) -> rule2)) -> rule6)) -> rule3)) -> rule5))] The mouse visits the mouse.[(((triple6) -> rule4))] The tiger visits the tiger.[(((triple11) -> rule6) OR ((((triple15) -> rule2)) -> rule6) OR ((((((triple13) -> rule4)) -> rule2)) -> rule6) OR ((((((((triple6) -> rule4) triple1) -> rule1)) -> rule2)) -> rule6))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
triple5
((triple7) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
((((((((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int4
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple7
((triple4) -> (rule6 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
((((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple8
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
((triple15) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
((((((triple6) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
triple12
The tiger is rough.
("tiger" "is" "rough" "+")
triple13
The tiger is young.
("tiger" "is" "young" "+")
triple14
((triple12) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple15
((triple13) -> (rule4 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
((((triple6) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
((triple5) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
((((((((((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
int4
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int5
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple6) -> (rule4 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple11) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
((((((triple13) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int3
((((((((triple6) -> (rule4 % int4)) triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int3
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int4