The mouse chases the tiger. The mouse is big. The mouse is kind. The mouse is rough. The mouse is round. The mouse is young. The mouse likes the tiger. The mouse visits the tiger. The tiger chases the mouse. The tiger is big. The tiger is kind. The tiger is rough. The tiger is round. The tiger is young. The tiger likes the mouse. The tiger visits the mouse. If someone chases the tiger then they like the tiger. If someone is kind then they like the mouse. If someone is round and they visit the tiger then the tiger likes the mouse. If the mouse visits the tiger and the tiger likes the mouse then the tiger is round. If someone is young then they chase the tiger. If someone visits the tiger and they chase the mouse then the tiger visits the mouse. If someone chases the tiger and the tiger likes the mouse then the tiger chases the mouse. If someone likes the tiger then they like the mouse.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone chases the tiger then they like the tiger.
((("someone" "chases" "tiger" "+")) -> ("someone" "likes" "tiger" "+"))
If someone is kind then they like the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is round and they visit the tiger then the tiger likes the mouse.
((("someone" "is" "round" "+") ("someone" "visits" "tiger" "+")) -> ("tiger" "likes" "mouse" "+"))
If the mouse visits the tiger and the tiger likes the mouse then the tiger is round.
((("mouse" "visits" "tiger" "+") ("tiger" "likes" "mouse" "+")) -> ("tiger" "is" "round" "+"))
If someone is young then they chase the tiger.
((("someone" "is" "young" "+")) -> ("someone" "chases" "tiger" "+"))
If someone visits the tiger and they chase the mouse then the tiger visits the mouse.
((("someone" "visits" "tiger" "+") ("someone" "chases" "mouse" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone chases the tiger and the tiger likes the mouse then the tiger chases the mouse.
((("someone" "chases" "tiger" "+") ("tiger" "likes" "mouse" "+")) -> ("tiger" "chases" "mouse" "+"))
If someone likes the tiger then they like the mouse.
((("someone" "likes" "tiger" "+")) -> ("someone" "likes" "mouse" "+"))
The mouse visits the tiger.
True
1
proof
[(triple8)]
("mouse" "visits" "tiger" "+")
triple8
The tiger is not round.
False
1
inv-proof
[(triple13 OR ((triple8 triple15) -> rule4) OR ((triple8 ((triple11) -> rule2)) -> rule4) OR ((triple8 ((triple5 triple8) -> rule3)) -> rule4) OR ((triple8 ((((((triple14) -> rule5)) -> rule1)) -> rule8)) -> rule4))]
("tiger" "is" "round" "-")
triple13
((triple8 triple15) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
((triple8 ((triple11) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
((triple8 ((triple5 triple8) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
((triple8 ((((((triple14) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int4
The mouse likes the mouse.
True
2
proof
[(((triple3) -> rule2) OR ((triple7) -> rule8) OR ((((triple1) -> rule1)) -> rule8) OR ((((((triple6) -> rule5)) -> rule1)) -> rule8))]
("mouse" "likes" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
((triple7) -> (rule8 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int3
The mouse does not like the mouse.
False
2
inv-proof
[(((triple3) -> rule2) OR ((triple7) -> rule8) OR ((((triple1) -> rule1)) -> rule8) OR ((((((triple6) -> rule5)) -> rule1)) -> rule8))]
("mouse" "likes" "mouse" "-")
((triple3) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
((triple7) -> (rule8 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int3
The tiger likes the tiger.
True
3
proof
[(((((triple14) -> rule5)) -> rule1))]
("tiger" "likes" "tiger" "+")
((((triple14) -> (rule5 % int2))) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger does not like the tiger.
False
3
inv-proof
[(((((triple14) -> rule5)) -> rule1))]
("tiger" "likes" "tiger" "-")
((((triple14) -> (rule5 % int2))) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The mouse chases the tiger.[(triple1 OR ((triple6) -> rule5))] The mouse is big.[(triple2)] The mouse is kind.[(triple3)] The mouse is rough.[(triple4)] The mouse is round.[(triple5)] The mouse is young.[(triple6)] The mouse likes the tiger.[(triple7 OR ((triple1) -> rule1) OR ((((triple6) -> rule5)) -> rule1))] The mouse visits the tiger.[(triple8)] The tiger chases the mouse.[(triple9 OR ((triple1 triple15) -> rule7) OR ((triple1 ((triple11) -> rule2)) -> rule7) OR ((triple1 ((triple5 triple8) -> rule3)) -> rule7) OR ((((triple14) -> rule5) triple15) -> rule7) OR ((((triple6) -> rule5) triple15) -> rule7) OR ((((triple14) -> rule5) ((triple11) -> rule2)) -> rule7) OR ((((triple14) -> rule5) ((triple5 triple8) -> rule3)) -> rule7) OR ((((triple6) -> rule5) ((triple11) -> rule2)) -> rule7) OR ((((triple6) -> rule5) ((triple5 triple8) -> rule3)) -> rule7) OR ((triple1 ((((((triple14) -> rule5)) -> rule1)) -> rule8)) -> rule7) OR ((((triple14) -> rule5) ((((((triple14) -> rule5)) -> rule1)) -> rule8)) -> rule7) OR ((((triple6) -> rule5) ((((((triple14) -> rule5)) -> rule1)) -> rule8)) -> rule7))] The tiger is big.[(triple10)] The tiger is kind.[(triple11)] The tiger is rough.[(triple12)] The tiger is round.[(triple13 OR ((triple8 triple15) -> rule4) OR ((triple8 ((triple11) -> rule2)) -> rule4) OR ((triple8 ((triple5 triple8) -> rule3)) -> rule4) OR ((triple8 ((((((triple14) -> rule5)) -> rule1)) -> rule8)) -> rule4))] The tiger is young.[(triple14)] The tiger likes the mouse.[(triple15 OR ((triple11) -> rule2) OR ((triple5 triple8) -> rule3) OR ((((((triple14) -> rule5)) -> rule1)) -> rule8))] The tiger visits the mouse.[(triple16)] @1: The mouse likes the mouse.[(((triple3) -> rule2) OR ((triple7) -> rule8) OR ((((triple1) -> rule1)) -> rule8) OR ((((((triple6) -> rule5)) -> rule1)) -> rule8))] The tiger chases the tiger.[(((triple14) -> rule5))] @2: The tiger likes the tiger.[(((((triple14) -> rule5)) -> rule1))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
((triple6) -> (rule5 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse is round.
("mouse" "is" "round" "+")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple7
((triple1) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple8
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple9
((triple1 triple15) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
((triple1 ((triple11) -> (rule2 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
((triple1 ((triple5 triple8) -> (rule3 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
((((triple14) -> (rule5 % int2)) triple15) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
((((triple6) -> (rule5 % int2)) triple15) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
((((triple14) -> (rule5 % int3)) ((triple11) -> (rule2 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
((((triple14) -> (rule5 % int3)) ((triple5 triple8) -> (rule3 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
((((triple6) -> (rule5 % int3)) ((triple11) -> (rule2 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int3
((((triple6) -> (rule5 % int3)) ((triple5 triple8) -> (rule3 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int3
((triple1 ((((((triple14) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int4
((((triple14) -> (rule5 % int4)) ((((((triple14) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int4
((((triple6) -> (rule5 % int5)) ((((((triple14) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int4
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int5
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger is round.
("tiger" "is" "round" "+")
triple13
((triple8 triple15) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
((triple8 ((triple11) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
((triple8 ((triple5 triple8) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
((triple8 ((((((triple14) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int4
The tiger is young.
("tiger" "is" "young" "+")
triple14
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple15
((triple11) -> (rule2 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
((triple5 triple8) -> (rule3 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
((((((triple14) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple16
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
((triple7) -> (rule8 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int3
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple14) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((triple14) -> (rule5 % int2))) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2