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