The cat eats the mouse. The cat is big. The cat is cold. The cat is green. The cat is red. The cat is rough. The cat likes the mouse. The cat sees the mouse. The mouse eats the cat. The mouse is big. The mouse is cold. The mouse is green. The mouse is not red. The mouse is rough. The mouse likes the cat. The mouse sees the cat. If something likes the cat and it is green then the cat is cold. If something sees the mouse then it likes the mouse. If something is big and it likes the cat then the cat eats the mouse. If something likes the cat and it sees the mouse then the mouse is big. If something likes the mouse and it is not cold then it sees the mouse. If something eats the mouse and it likes the cat then it sees the mouse. If something likes the mouse and it is not red then it is big. If something is big then it eats the mouse.
The cat eats the mouse.
("cat" "eats" "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 red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "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 not red.
("mouse" "is" "red" "-")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If something likes the cat and it is green then the cat is cold.
((("something" "likes" "cat" "+") ("something" "is" "green" "+")) -> ("cat" "is" "cold" "+"))
If something sees the mouse then it likes the mouse.
((("something" "sees" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
If something is big and it likes the cat then the cat eats the mouse.
((("something" "is" "big" "+") ("something" "likes" "cat" "+")) -> ("cat" "eats" "mouse" "+"))
If something likes the cat and it sees the mouse then the mouse is big.
((("something" "likes" "cat" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If something likes the mouse and it is not cold then it sees the mouse.
((("something" "likes" "mouse" "+") ("something" "is" "cold" "~")) -> ("something" "sees" "mouse" "+"))
If something eats the mouse and it likes the cat then it sees the mouse.
((("something" "eats" "mouse" "+") ("something" "likes" "cat" "+")) -> ("something" "sees" "mouse" "+"))
If something likes the mouse and it is not red then it is big.
((("something" "likes" "mouse" "+") ("something" "is" "red" "~")) -> ("something" "is" "big" "+"))
If something is big then it eats the mouse.
((("something" "is" "big" "+")) -> ("something" "eats" "mouse" "+"))
The mouse is big.
True
1
proof
[(triple10)]
("mouse" "is" "big" "+")
triple10
The cat is not rough.
False
1
inv-proof
[(triple6)]
("cat" "is" "rough" "-")
triple6
The mouse eats the mouse.
True
2
proof
[(((triple10) -> rule8))]
("mouse" "eats" "mouse" "+")
((triple10) -> (rule8 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse does not eat the mouse.
False
2
inv-proof
[(((triple10) -> rule8))]
("mouse" "eats" "mouse" "-")
((triple10) -> (rule8 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse sees the mouse.
True
4
proof
[(((((triple10) -> rule8) triple15) -> rule6))]
("mouse" "sees" "mouse" "+")
((((triple10) -> (rule8 % int2)) triple15) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse does not see the mouse.
False
4
inv-proof
[(((((triple10) -> rule8) triple15) -> rule6))]
("mouse" "sees" "mouse" "-")
((((triple10) -> (rule8 % int2)) triple15) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse likes the mouse.
True
5
proof
[(((((((triple10) -> rule8) triple15) -> rule6)) -> rule2))]
("mouse" "likes" "mouse" "+")
((((((triple10) -> (rule8 % int3)) triple15) -> (rule6 % int2))) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3
The mouse does not like the mouse.
False
5
inv-proof
[(((((((triple10) -> rule8) triple15) -> rule6)) -> rule2))]
("mouse" "likes" "mouse" "-")
((((((triple10) -> (rule8 % int3)) triple15) -> (rule6 % int2))) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3
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 cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat eats the mouse.[(triple1 OR ((triple2) -> rule8) OR ((triple10 triple15) -> rule3))] The cat is big.[(triple2)] The cat is cold.[(triple3 OR ((triple15 triple12) -> rule1))] The cat is green.[(triple4)] The cat is red.[(triple5)] The cat is rough.[(triple6)] The cat likes the mouse.[(triple7 OR ((triple8) -> rule2))] The cat sees the mouse.[(triple8)] The mouse eats the cat.[(triple9)] The mouse is big.[(triple10)] The mouse is cold.[(triple11)] The mouse is green.[(triple12)] The mouse is not red.[(triple13)] The mouse is rough.[(triple14)] The mouse likes the cat.[(triple15)] The mouse sees the cat.[(triple16)] @1: The mouse eats the mouse.[(((triple10) -> rule8))] @2: The mouse sees the mouse.[(((((triple10) -> rule8) triple15) -> rule6))] @3: The mouse likes the mouse.[(((((((triple10) -> rule8) triple15) -> rule6)) -> rule2))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
((triple2) -> (rule8 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
((triple10 triple15) -> (rule3 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
((triple15 triple12) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is green.
("cat" "is" "green" "+")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple7
((triple8) -> (rule2 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple8
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple9
The mouse is big.
("mouse" "is" "big" "+")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The mouse is green.
("mouse" "is" "green" "+")
triple12
The mouse is not red.
("mouse" "is" "red" "-")
triple13
The mouse is rough.
("mouse" "is" "rough" "+")
triple14
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple15
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple16
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple10) -> (rule8 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple10) -> (rule8 % int2)) triple15) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((triple10) -> (rule8 % int3)) triple15) -> (rule6 % int2))) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3