The cat is round. The cat is young. The cat likes the mouse. The cat needs the mouse. The cat sees the mouse. The mouse is not blue. The mouse is cold. The mouse is green. The mouse is not round. The mouse does not like the cat. The mouse needs the cat. The mouse sees the cat. If someone is round then they see the cat. All young people are round. If someone is young and they like the cat then they need the mouse. If someone is young and they see the cat then they are not cold. If someone sees the mouse and they need the cat then they are blue. If the cat likes the mouse then the cat is green.
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse is not blue.
("mouse" "is" "blue" "-")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is not round.
("mouse" "is" "round" "-")
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone is round then they see the cat.
((("someone" "is" "round" "+")) -> ("someone" "sees" "cat" "+"))
All young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is young and they like the cat then they need the mouse.
((("someone" "is" "young" "+") ("someone" "likes" "cat" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is young and they see the cat then they are not cold.
((("someone" "is" "young" "+") ("someone" "sees" "cat" "+")) -> ("someone" "is" "cold" "-"))
If someone sees the mouse and they need the cat then they are blue.
((("someone" "sees" "mouse" "+") ("someone" "needs" "cat" "+")) -> ("someone" "is" "blue" "+"))
If the cat likes the mouse then the cat is green.
((("cat" "likes" "mouse" "+")) -> ("cat" "is" "green" "+"))
The cat likes the mouse.
True
1
proof
[(triple3)]
("cat" "likes" "mouse" "+")
triple3
The cat does not like the mouse.
False
1
inv-proof
[(triple3)]
("cat" "likes" "mouse" "-")
triple3
The cat is green.
True
2
proof
[(((triple3) -> rule6))]
("cat" "is" "green" "+")
((triple3) -> (rule6 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple1) -> rule1) OR ((((triple2) -> rule2)) -> rule1))]
("cat" "sees" "cat" "-")
((triple1) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is not cold.
True
4
proof
[(((triple2 ((triple1) -> rule1)) -> rule4) OR ((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule4))]
("cat" "is" "cold" "-")
((triple2 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat is cold.
False
4
inv-proof
[(((triple2 ((triple1) -> rule1)) -> rule4) OR ((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule4))]
("cat" "is" "cold" "+")
((triple2 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "blue" "-")
The mouse needs the mouse.
Unknown
rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is round.[(triple1 OR ((triple2) -> rule2))] The cat is young.[(triple2)] The cat likes the mouse.[(triple3)] The cat needs the mouse.[(triple4)] The cat sees the mouse.[(triple5)] The mouse does not like the cat.[(triple10)] The mouse is cold.[(triple7)] The mouse is green.[(triple8)] The mouse is not blue.[(triple6)] The mouse is not round.[(triple9)] The mouse needs the cat.[(triple11)] The mouse sees the cat.[(triple12)] @1: The cat is green.[(((triple3) -> rule6))] The cat sees the cat.[(((triple1) -> rule1) OR ((((triple2) -> rule2)) -> rule1))] @2: The cat is not cold.[(((triple2 ((triple1) -> rule1)) -> rule4) OR ((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule4))]
The cat is round.
("cat" "is" "round" "+")
triple1
((triple2) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is young.
("cat" "is" "young" "+")
triple2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
triple8
The mouse is not blue.
("mouse" "is" "blue" "-")
triple6
The mouse is not round.
("mouse" "is" "round" "-")
triple9
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple11
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple12
The cat is green.
("cat" "is" "green" "+")
((triple3) -> (rule6 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple1) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is not cold.
("cat" "is" "cold" "-")
((triple2 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3