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