The cat is kind. The cat is nice. The cat is red. The cat is round. The cat is young. If the cat is nice and the cat is round then the cat is young. If someone is young then they are kind. All kind, round people are young.
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
If the cat is nice and the cat is round then the cat is young.
((("cat" "is" "nice" "+") ("cat" "is" "round" "+")) -> ("cat" "is" "young" "+"))
If someone is young then they are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All kind, round people are young.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
The cat is red.
True
1
proof
[(triple3)]
("cat" "is" "red" "+")
triple3
The cat is not nice.
False
1
inv-proof
[(triple2)]
("cat" "is" "nice" "-")
triple2
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is kind.[(triple1 OR ((triple5) -> rule2) OR ((((triple2 triple4) -> rule1)) -> rule2))] The cat is nice.[(triple2)] The cat is red.[(triple3)] The cat is round.[(triple4)] The cat is young.[(triple5 OR ((triple1 triple4) -> rule3) OR ((triple2 triple4) -> rule1))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
((triple5) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((((triple2 triple4) -> (rule1 % int2))) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
((triple1 triple4) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple2 triple4) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1