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