The cat is cold. The cat is kind. The cat is rough. The cat needs the squirrel. The cat sees the squirrel. The cat visits the squirrel. The squirrel is cold. The squirrel is nice. The squirrel is young. The squirrel needs the cat. The squirrel sees the cat. The squirrel visits the cat. If someone is cold then they visit the cat. If someone is young then they need the cat.
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If someone is cold then they visit the cat.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "cat" "+"))
If someone is young then they need the cat.
((("someone" "is" "young" "+")) -> ("someone" "needs" "cat" "+"))
The squirrel needs the cat.
True
1
proof
[(triple10 OR ((triple9) -> rule2))]
("squirrel" "needs" "cat" "+")
triple10
((triple9) -> (rule2 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The squirrel is not cold.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "cold" "-")
triple7
The cat visits the cat.
True
2
proof
[(((triple1) -> rule1))]
("cat" "visits" "cat" "+")
((triple1) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "visits" "cat" "-")
((triple1) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "cat" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The cat is cold.[(triple1)] The cat is kind.[(triple2)] The cat is rough.[(triple3)] The cat needs the squirrel.[(triple4)] The cat sees the squirrel.[(triple5)] The cat visits the squirrel.[(triple6)] The squirrel is cold.[(triple7)] The squirrel is nice.[(triple8)] The squirrel is young.[(triple9)] The squirrel needs the cat.[(triple10 OR ((triple9) -> rule2))] The squirrel sees the cat.[(triple11)] The squirrel visits the cat.[(triple12 OR ((triple7) -> rule1))] @1: The cat visits the cat.[(((triple1) -> rule1))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple4
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple5
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple6
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple7
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple8
The squirrel is young.
("squirrel" "is" "young" "+")
triple9
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple10
((triple9) -> (rule2 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple11
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple12
((triple7) -> (rule1 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple1) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1