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