The dog chases the mouse. The dog chases the tiger. The dog is big. The dog is kind. The dog likes the tiger. The dog does not see the mouse. The dog sees the tiger. The mouse chases the dog. The mouse chases the tiger. The mouse is blue. The mouse is rough. The mouse likes the dog. The mouse likes the tiger. The mouse sees the tiger. The tiger likes the mouse. If the tiger chases the mouse then the mouse likes the dog. If something chases the tiger then the tiger sees the dog. If the tiger is round then the tiger does not like the dog. If the mouse chases the dog and the mouse sees the dog then the dog is not big. If something is big then it sees the tiger. All blue things are kind. If something sees the tiger then the tiger is blue. If something sees the mouse then the mouse does not chase the dog.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If the tiger chases the mouse then the mouse likes the dog.
((("tiger" "chases" "mouse" "+")) -> ("mouse" "likes" "dog" "+"))
If something chases the tiger then the tiger sees the dog.
((("something" "chases" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
If the tiger is round then the tiger does not like the dog.
((("tiger" "is" "round" "+")) -> ("tiger" "likes" "dog" "-"))
If the mouse chases the dog and the mouse sees the dog then the dog is not big.
((("mouse" "chases" "dog" "+") ("mouse" "sees" "dog" "+")) -> ("dog" "is" "big" "-"))
If something is big then it sees the tiger.
((("something" "is" "big" "+")) -> ("something" "sees" "tiger" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something sees the tiger then the tiger is blue.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If something sees the mouse then the mouse does not chase the dog.
((("something" "sees" "mouse" "+")) -> ("mouse" "chases" "dog" "-"))
The mouse sees the tiger.
True
1
proof
[(triple14)]
("mouse" "sees" "tiger" "+")
triple14
The mouse does not chase the dog.
False
1
inv-proof
[(triple8)]
("mouse" "chases" "dog" "-")
triple8
The tiger is blue.
True
2
proof
[(((triple14) -> rule7) OR ((triple7) -> rule7) OR ((((triple3) -> rule5)) -> rule7))]
("tiger" "is" "blue" "+")
((triple14) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
((triple7) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2
The mouse is not kind.
False
2
inv-proof
[(((triple10) -> rule6))]
("mouse" "is" "kind" "-")
((triple10) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The tiger is kind.
True
3
proof
[(((((triple14) -> rule7)) -> rule6) OR ((((triple7) -> rule7)) -> rule6) OR ((((((triple3) -> rule5)) -> rule7)) -> rule6))]
("tiger" "is" "kind" "+")
((((triple14) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((((triple7) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int3
The tiger is not kind.
False
3
inv-proof
[(((((triple14) -> rule7)) -> rule6) OR ((((triple7) -> rule7)) -> rule6) OR ((((((triple3) -> rule5)) -> rule7)) -> rule6))]
("tiger" "is" "kind" "-")
((((triple14) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((((triple7) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int3
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
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 big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The dog chases the mouse.[(triple1)] The dog chases the tiger.[(triple2)] The dog does not see the mouse.[(triple6)] The dog is big.[(triple3)] The dog is kind.[(triple4)] The dog likes the tiger.[(triple5)] The dog sees the tiger.[(triple7 OR ((triple3) -> rule5))] The mouse chases the dog.[(triple8)] The mouse chases the tiger.[(triple9)] The mouse is blue.[(triple10)] The mouse is rough.[(triple11)] The mouse likes the dog.[(triple12)] The mouse likes the tiger.[(triple13)] The mouse sees the tiger.[(triple14)] The tiger likes the mouse.[(triple15)] @1: The mouse is kind.[(((triple10) -> rule6))] The tiger is blue.[(((triple14) -> rule7) OR ((triple7) -> rule7) OR ((((triple3) -> rule5)) -> rule7))] The tiger sees the dog.[(((triple2) -> rule2) OR ((triple9) -> rule2))] @2: The tiger is kind.[(((((triple14) -> rule7)) -> rule6) OR ((((triple7) -> rule7)) -> rule6) OR ((((((triple3) -> rule5)) -> rule7)) -> rule6))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple2
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
triple6
The dog is big.
("dog" "is" "big" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple5
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple7
((triple3) -> (rule5 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple8
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is rough.
("mouse" "is" "rough" "+")
triple11
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple12
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple13
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple14
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple15
The mouse is kind.
("mouse" "is" "kind" "+")
((triple10) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple14) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
((triple7) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((triple2) -> (rule2 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
((triple9) -> (rule2 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple14) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((((triple7) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int3