The dog does not like the mouse. The mouse sees the tiger. The tiger is big. If something is red then it sees the tiger. If something likes the tiger and it is not big then it chases the tiger. If something sees the tiger then it likes the tiger. If something is red then it likes the tiger. If something chases the mouse then the mouse is red. If something sees the tiger and the tiger is not big then it does not like the mouse. If something likes the tiger then the tiger chases the mouse. If the tiger does not like the mouse then the tiger sees the dog.
The dog does not like the mouse.
("dog" "likes" "mouse" "-")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
If something is red then it sees the tiger.
((("something" "is" "red" "+")) -> ("something" "sees" "tiger" "+"))
If something likes the tiger and it is not big then it chases the tiger.
((("something" "likes" "tiger" "+") ("something" "is" "big" "~")) -> ("something" "chases" "tiger" "+"))
If something sees the tiger then it likes the tiger.
((("something" "sees" "tiger" "+")) -> ("something" "likes" "tiger" "+"))
If something is red then it likes the tiger.
((("something" "is" "red" "+")) -> ("something" "likes" "tiger" "+"))
If something chases the mouse then the mouse is red.
((("something" "chases" "mouse" "+")) -> ("mouse" "is" "red" "+"))
If something sees the tiger and the tiger is not big then it does not like the mouse.
((("something" "sees" "tiger" "+") ("tiger" "is" "big" "~")) -> ("something" "likes" "mouse" "-"))
If something likes the tiger then the tiger chases the mouse.
((("something" "likes" "tiger" "+")) -> ("tiger" "chases" "mouse" "+"))
If the tiger does not like the mouse then the tiger sees the dog.
((("tiger" "likes" "mouse" "~")) -> ("tiger" "sees" "dog" "+"))
The mouse sees the tiger.
True
1
proof
[(triple2)]
("mouse" "sees" "tiger" "+")
triple2
The dog likes the mouse.
False
1
inv-proof
[(triple1)]
("dog" "likes" "mouse" "+")
triple1
The mouse likes the tiger.
True
2
proof
[(((triple2) -> rule3))]
("mouse" "likes" "tiger" "+")
((triple2) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse does not like the tiger.
False
2
inv-proof
[(((triple2) -> rule3))]
("mouse" "likes" "tiger" "-")
((triple2) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The tiger chases the mouse.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("tiger" "chases" "mouse" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The tiger does not chase the mouse.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7))]
("tiger" "chases" "mouse" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse is red.
True
4
proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule5))]
("mouse" "is" "red" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The mouse is not red.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule5))]
("mouse" "is" "red" "-")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The dog does not like the tiger.
Unknown
inv-rconc
[@2: The dog likes the tiger.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("dog" "likes" "tiger" "-")
The tiger likes the tiger.
Unknown
rconc
[@2: The tiger likes the tiger.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("tiger" "likes" "tiger" "+")
The dog does not chase the tiger.
Unknown
inv-rconc
[@1: The dog chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "tiger" "-")
The tiger chases the tiger.
Unknown
rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "tiger" "+")
The mouse does not see the dog.
Unknown
inv-random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The dog sees the mouse.
Unknown
random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "+")
@0: The dog does not like the mouse.[(triple1)] The mouse sees the tiger.[(triple2)] The tiger is big.[(triple3)] @1: The mouse likes the tiger.[(((triple2) -> rule3))] @2: The tiger chases the mouse.[(((((triple2) -> rule3)) -> rule7))] @3: The mouse is red.[(((((((triple2) -> rule3)) -> rule7)) -> rule5))]
The dog does not like the mouse.
("dog" "likes" "mouse" "-")
triple1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple2
The tiger is big.
("tiger" "is" "big" "+")
triple3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((triple2) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3