The cat chases the mouse. The cat is big. The cat is cold. The cat is green. The cat is kind. The cat is round. The cat needs the mouse. The cat sees the mouse. The mouse chases the cat. The mouse is big. The mouse is cold. The mouse is green. The mouse is kind. The mouse is round. The mouse needs the cat. The mouse sees the cat. If the mouse is kind then the mouse needs the cat. If something chases the mouse then it sees the mouse. If something sees the mouse and it is big then it is green. If the cat chases the mouse and the mouse needs the cat then the mouse is big. If something is cold and it needs the cat then it is kind. If something is green then it needs the mouse.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
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 is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If the mouse is kind then the mouse needs the cat.
((("mouse" "is" "kind" "+")) -> ("mouse" "needs" "cat" "+"))
If something chases the mouse then it sees the mouse.
((("something" "chases" "mouse" "+")) -> ("something" "sees" "mouse" "+"))
If something sees the mouse and it is big then it is green.
((("something" "sees" "mouse" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If the cat chases the mouse and the mouse needs the cat then the mouse is big.
((("cat" "chases" "mouse" "+") ("mouse" "needs" "cat" "+")) -> ("mouse" "is" "big" "+"))
If something is cold and it needs the cat then it is kind.
((("something" "is" "cold" "+") ("something" "needs" "cat" "+")) -> ("something" "is" "kind" "+"))
If something is green then it needs the mouse.
((("something" "is" "green" "+")) -> ("something" "needs" "mouse" "+"))
The mouse is cold.
True
1
proof
[(triple11)]
("mouse" "is" "cold" "+")
triple11
The cat is not kind.
False
1
inv-proof
[(triple5)]
("cat" "is" "kind" "-")
triple5
The mouse needs the mouse.
True
2
proof
[(((triple12) -> rule6))]
("mouse" "needs" "mouse" "+")
((triple12) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse does not need the mouse.
False
2
inv-proof
[(((triple12) -> rule6))]
("mouse" "needs" "mouse" "-")
((triple12) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat chases the mouse.[(triple1)] The cat is big.[(triple2)] The cat is cold.[(triple3)] The cat is green.[(triple4 OR ((triple8 triple2) -> rule3) OR ((((triple1) -> rule2) triple2) -> rule3))] The cat is kind.[(triple5)] The cat is round.[(triple6)] The cat needs the mouse.[(triple7 OR ((triple4) -> rule6) OR ((((triple8 triple2) -> rule3)) -> rule6) OR ((((((triple1) -> rule2) triple2) -> rule3)) -> rule6))] The cat sees the mouse.[(triple8 OR ((triple1) -> rule2))] The mouse chases the cat.[(triple9)] The mouse is big.[(triple10 OR ((triple1 triple15) -> rule4) OR ((triple1 ((triple13) -> rule1)) -> rule4))] The mouse is cold.[(triple11)] The mouse is green.[(triple12)] The mouse is kind.[(triple13 OR ((triple11 triple15) -> rule5))] The mouse is round.[(triple14)] The mouse needs the cat.[(triple15 OR ((triple13) -> rule1))] The mouse sees the cat.[(triple16)] @1: The mouse needs the mouse.[(((triple12) -> rule6))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
triple4
((triple8 triple2) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
triple5
The cat is round.
("cat" "is" "round" "+")
triple6
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple7
((triple4) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
((((triple8 triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
((((((triple1) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple8
((triple1) -> (rule2 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple9
The mouse is big.
("mouse" "is" "big" "+")
triple10
((triple1 triple15) -> (rule4 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
((triple1 ((triple13) -> (rule1 % int2))) -> (rule4 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The mouse is green.
("mouse" "is" "green" "+")
triple12
The mouse is kind.
("mouse" "is" "kind" "+")
triple13
((triple11 triple15) -> (rule5 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
triple14
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple15
((triple13) -> (rule1 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple16
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple12) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1