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