The cat is big. The cat does not see the mouse. The mouse chases the cat. The mouse chases the rabbit. The mouse is big. The mouse is blue. The mouse likes the cat. The mouse likes the rabbit. The mouse sees the rabbit. The rabbit does not chase the cat. The rabbit is big. The rabbit is not young. The rabbit likes the cat. The rabbit likes the mouse. The rabbit sees the cat. If someone is cold then they do not chase the rabbit. If someone is big and they chase the mouse then they see the rabbit. If someone sees the cat and they do not chase the cat then they like the rabbit. Green people are not young. If someone chases the mouse then they are not young. If someone sees the cat then the cat is cold. If the rabbit is young and the rabbit is blue then the rabbit sees the cat. If someone likes the cat and the cat chases the rabbit then they chase the mouse.
The cat is big.
("cat" "is" "big" "+")
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is not young.
("rabbit" "is" "young" "-")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If someone is cold then they do not chase the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "rabbit" "-"))
If someone is big and they chase the mouse then they see the rabbit.
((("someone" "is" "big" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone sees the cat and they do not chase the cat then they like the rabbit.
((("someone" "sees" "cat" "+") ("someone" "chases" "cat" "~")) -> ("someone" "likes" "rabbit" "+"))
Green people are not young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "-"))
If someone chases the mouse then they are not young.
((("someone" "chases" "mouse" "+")) -> ("someone" "is" "young" "-"))
If someone sees the cat then the cat is cold.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "cold" "+"))
If the rabbit is young and the rabbit is blue then the rabbit sees the cat.
((("rabbit" "is" "young" "+") ("rabbit" "is" "blue" "+")) -> ("rabbit" "sees" "cat" "+"))
If someone likes the cat and the cat chases the rabbit then they chase the mouse.
((("someone" "likes" "cat" "+") ("cat" "chases" "rabbit" "+")) -> ("someone" "chases" "mouse" "+"))
The mouse sees the rabbit.
True
1
proof
[(triple9)]
("mouse" "sees" "rabbit" "+")
triple9
The cat is not big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "-")
triple1
The cat is cold.
True
2
proof
[(((triple15) -> rule6))]
("cat" "is" "cold" "+")
((triple15) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple15) -> rule6))]
("cat" "is" "cold" "-")
((triple15) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat does not chase the rabbit.
True
3
proof
[(((((triple15) -> rule6)) -> rule1))]
("cat" "chases" "rabbit" "-")
((((triple15) -> (rule6 % int2))) -> (rule1 % int1))
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat chases the rabbit.
False
3
inv-proof
[(((((triple15) -> rule6)) -> rule1))]
("cat" "chases" "rabbit" "+")
((((triple15) -> (rule6 % int2))) -> (rule1 % int1))
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat does not chase the mouse.
Unknown
inv-rconc
[@1: The cat chases the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "chases" "mouse" "-")
The cat likes the rabbit.
Unknown
rconc
[@1: The cat likes the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@2: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The mouse sees the cat.
Unknown
random
[@0: The mouse sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cat" "+")
@0: The cat does not see the mouse.[(triple2)] The cat is big.[(triple1)] The mouse chases the cat.[(triple3)] The mouse chases the rabbit.[(triple4)] The mouse is big.[(triple5)] The mouse is blue.[(triple6)] The mouse likes the cat.[(triple7)] The mouse likes the rabbit.[(triple8)] The mouse sees the rabbit.[(triple9)] The rabbit does not chase the cat.[(triple10)] The rabbit is big.[(triple11)] The rabbit is not young.[(triple12)] The rabbit likes the cat.[(triple13)] The rabbit likes the mouse.[(triple14)] The rabbit sees the cat.[(triple15)] @1: The cat is cold.[(((triple15) -> rule6))] The rabbit likes the rabbit.[(((triple15 triple10) -> rule3))] @2: The cat does not chase the rabbit.[(((((triple15) -> rule6)) -> rule1))]
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
triple2
The cat is big.
("cat" "is" "big" "+")
triple1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple3
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple4
The mouse is big.
("mouse" "is" "big" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple7
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple8
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple9
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
triple10
The rabbit is big.
("rabbit" "is" "big" "+")
triple11
The rabbit is not young.
("rabbit" "is" "young" "-")
triple12
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple13
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple14
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple15
The cat is cold.
("cat" "is" "cold" "+")
((triple15) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple15 triple10) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
((((triple15) -> (rule6 % int2))) -> (rule1 % int1))
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2