The cat is big. The mouse visits the tiger. The tiger is round. If someone chases the cat then the cat visits the tiger. If someone chases the tiger and the tiger is not blue then the tiger does not like the cat. If someone chases the cat and the cat is not round then they visit the mouse. If someone visits the tiger then they chase the cat. If someone is big then they are nice. If someone likes the mouse then the mouse is not blue. If the cat visits the tiger and the tiger visits the cat then the tiger chases the mouse. If the cat visits the mouse and the cat is not blue then the mouse visits the cat.
The cat is big.
("cat" "is" "big" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone chases the cat then the cat visits the tiger.
((("someone" "chases" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If someone chases the tiger and the tiger is not blue then the tiger does not like the cat.
((("someone" "chases" "tiger" "+") ("tiger" "is" "blue" "~")) -> ("tiger" "likes" "cat" "-"))
If someone chases the cat and the cat is not round then they visit the mouse.
((("someone" "chases" "cat" "+") ("cat" "is" "round" "~")) -> ("someone" "visits" "mouse" "+"))
If someone visits the tiger then they chase the cat.
((("someone" "visits" "tiger" "+")) -> ("someone" "chases" "cat" "+"))
If someone is big then they are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone likes the mouse then the mouse is not blue.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "blue" "-"))
If the cat visits the tiger and the tiger visits the cat then the tiger chases the mouse.
((("cat" "visits" "tiger" "+") ("tiger" "visits" "cat" "+")) -> ("tiger" "chases" "mouse" "+"))
If the cat visits the mouse and the cat is not blue then the mouse visits the cat.
((("cat" "visits" "mouse" "+") ("cat" "is" "blue" "~")) -> ("mouse" "visits" "cat" "+"))
The mouse visits the tiger.
True
1
proof
[(triple2)]
("mouse" "visits" "tiger" "+")
triple2
The cat is not big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "-")
triple1
The cat is nice.
True
2
proof
[(((triple1) -> rule5))]
("cat" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is not nice.
False
2
inv-proof
[(((triple1) -> rule5))]
("cat" "is" "nice" "-")
((triple1) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat visits the tiger.
True
3
proof
[(((((triple2) -> rule4)) -> rule1))]
("cat" "visits" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The cat does not visit the tiger.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule1))]
("cat" "visits" "tiger" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The cat chases the cat.
True
4
proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule4))]
("cat" "chases" "cat" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The cat does not chase the cat.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule4))]
("cat" "chases" "cat" "-")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The tiger does not chase the mouse.
Unknown
inv-rconc
[@1: The tiger chases the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "chases" "mouse" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "nice" "+")
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "nice" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The tiger visits the cat.
Unknown
random
[@0: The tiger visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "cat" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The cat likes the mouse.
Unknown
random
[@0: The cat likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "mouse" "+")
@0: The cat is big.[(triple1)] The mouse visits the tiger.[(triple2)] The tiger is round.[(triple3)] @1: The cat is nice.[(((triple1) -> rule5))] The mouse chases the cat.[(((triple2) -> rule4))] @2: The cat visits the tiger.[(((((triple2) -> rule4)) -> rule1))] @3: The cat chases the cat.[(((((((triple2) -> rule4)) -> rule1)) -> rule4))]
The cat is big.
("cat" "is" "big" "+")
triple1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple2
The tiger is round.
("tiger" "is" "round" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
((triple2) -> (rule4 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3