The cat eats the mouse. The cat is blue. The cat is kind. The cow eats the cat. The cow is blue. The cow is kind. The cow sees the cat. The cow sees the squirrel. The cow visits the cat. The mouse sees the cow. The mouse visits the cow. The squirrel is blue. The squirrel is cold. The squirrel is red. The squirrel sees the mouse. The squirrel visits the mouse. If something is cold and blue then it is kind.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If something is cold and blue then it is kind.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
The cow sees the cat.
True
1
proof
[(triple7)]
("cow" "sees" "cat" "+")
triple7
The squirrel is not cold.
False
1
inv-proof
[(triple13)]
("squirrel" "is" "cold" "-")
triple13
The squirrel is kind.
True
3
proof
[(((triple13 triple12) -> rule1))]
("squirrel" "is" "kind" "+")
((triple13 triple12) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is not kind.
False
3
inv-proof
[(((triple13 triple12) -> rule1))]
("squirrel" "is" "kind" "-")
((triple13 triple12) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "kind" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cat eats the mouse.[(triple1)] The cat is blue.[(triple2)] The cat is kind.[(triple3)] The cow eats the cat.[(triple4)] The cow is blue.[(triple5)] The cow is kind.[(triple6)] The cow sees the cat.[(triple7)] The cow sees the squirrel.[(triple8)] The cow visits the cat.[(triple9)] The mouse sees the cow.[(triple10)] The mouse visits the cow.[(triple11)] The squirrel is blue.[(triple12)] The squirrel is cold.[(triple13)] The squirrel is red.[(triple14)] The squirrel sees the mouse.[(triple15)] The squirrel visits the mouse.[(triple16)] @1: The squirrel is kind.[(((triple13 triple12) -> rule1))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cow eats the cat.
("cow" "eats" "cat" "+")
triple4
The cow is blue.
("cow" "is" "blue" "+")
triple5
The cow is kind.
("cow" "is" "kind" "+")
triple6
The cow sees the cat.
("cow" "sees" "cat" "+")
triple7
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple8
The cow visits the cat.
("cow" "visits" "cat" "+")
triple9
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple10
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple11
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple12
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple13
The squirrel is red.
("squirrel" "is" "red" "+")
triple14
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple15
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple16
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple13 triple12) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1