The cat is rough. The cat needs the squirrel. The squirrel is green. The squirrel is not rough. The squirrel is young. The squirrel needs the cat. The squirrel visits the cat. If someone sees the squirrel and the squirrel visits the cat then the squirrel is not rough. If the squirrel needs the cat and the cat visits the squirrel then the cat needs the squirrel. If someone sees the cat then the cat is kind. If someone is rough and they visit the cat then they are young. If someone is kind then they need the squirrel. If the squirrel needs the cat and the squirrel is not kind then the squirrel sees the cat. If someone is young then they see the cat. If someone needs the cat and they are young then they visit the cat.
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is not rough.
("squirrel" "is" "rough" "-")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If someone sees the squirrel and the squirrel visits the cat then the squirrel is not rough.
((("someone" "sees" "squirrel" "+") ("squirrel" "visits" "cat" "+")) -> ("squirrel" "is" "rough" "-"))
If the squirrel needs the cat and the cat visits the squirrel then the cat needs the squirrel.
((("squirrel" "needs" "cat" "+") ("cat" "visits" "squirrel" "+")) -> ("cat" "needs" "squirrel" "+"))
If someone sees the cat then the cat is kind.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "kind" "+"))
If someone is rough and they visit the cat then they are young.
((("someone" "is" "rough" "+") ("someone" "visits" "cat" "+")) -> ("someone" "is" "young" "+"))
If someone is kind then they need the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "squirrel" "+"))
If the squirrel needs the cat and the squirrel is not kind then the squirrel sees the cat.
((("squirrel" "needs" "cat" "+") ("squirrel" "is" "kind" "~")) -> ("squirrel" "sees" "cat" "+"))
If someone is young then they see the cat.
((("someone" "is" "young" "+")) -> ("someone" "sees" "cat" "+"))
If someone needs the cat and they are young then they visit the cat.
((("someone" "needs" "cat" "+") ("someone" "is" "young" "+")) -> ("someone" "visits" "cat" "+"))
The cat needs the squirrel.
True
1
proof
[(triple2 OR ((((((triple5) -> rule7)) -> rule3)) -> rule5))]
("cat" "needs" "squirrel" "+")
triple2
((((((triple5) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int3
The squirrel does not visit the cat.
False
1
inv-proof
[(triple7 OR ((triple6 triple5) -> rule8))]
("squirrel" "visits" "cat" "-")
triple7
((triple6 triple5) -> (rule8 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel sees the cat.
True
2
proof
[(((triple5) -> rule7))]
("squirrel" "sees" "cat" "+")
((triple5) -> (rule7 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The squirrel does not see the cat.
False
2
inv-proof
[(((triple5) -> rule7))]
("squirrel" "sees" "cat" "-")
((triple5) -> (rule7 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The cat is kind.
True
3
proof
[(((((triple5) -> rule7)) -> rule3))]
("cat" "is" "kind" "+")
((((triple5) -> (rule7 % int2))) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The cat is not kind.
False
3
inv-proof
[(((((triple5) -> rule7)) -> rule3))]
("cat" "is" "kind" "-")
((((triple5) -> (rule7 % int2))) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The cat does not see the cat.
Unknown
inv-rconc
[@3: The cat sees the cat.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule8 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "visits" "cat" "+")
The cat is not young.
Unknown
inv-rconc
[@2: The cat is young.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("cat" "is" "young" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat is rough.[(triple1)] The cat needs the squirrel.[(triple2 OR ((((((triple5) -> rule7)) -> rule3)) -> rule5))] The squirrel is green.[(triple3)] The squirrel is not rough.[(triple4)] The squirrel is young.[(triple5)] The squirrel needs the cat.[(triple6)] The squirrel visits the cat.[(triple7 OR ((triple6 triple5) -> rule8))] @1: The squirrel sees the cat.[(((triple5) -> rule7))] @2: The cat is kind.[(((((triple5) -> rule7)) -> rule3))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple2
((((((triple5) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
triple3
The squirrel is not rough.
("squirrel" "is" "rough" "-")
triple4
The squirrel is young.
("squirrel" "is" "young" "+")
triple5
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple6
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple7
((triple6 triple5) -> (rule8 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((triple5) -> (rule7 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
((((triple5) -> (rule7 % int2))) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2