The cat is kind. The cat is not nice. The cat is young. All rough, kind people are round. Nice, young people are round. If someone is round and nice then they are not rough. Kind people are rough. If someone is round then they are young. Rough people are young. All rough people are young. All nice, young people are kind.
The cat is kind.
("cat" "is" "kind" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat is young.
("cat" "is" "young" "+")
All rough, kind people are round.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Nice, young people are round.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is round and nice then they are not rough.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "-"))
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
All rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
All nice, young people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
The cat is kind.
True
1
proof
[(triple1)]
("cat" "is" "kind" "+")
triple1
The cat is not kind.
False
1
inv-proof
[(triple1)]
("cat" "is" "kind" "-")
triple1
The cat is rough.
True
2
proof
[(((triple1) -> rule4))]
("cat" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is not rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("cat" "is" "rough" "-")
((triple1) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "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)] The cat is not nice.[(triple2)] The cat is young.[(triple3 OR ((((triple1) -> rule4)) -> rule6) OR ((((triple1) -> rule4)) -> rule7) OR ((((((triple1) -> rule4) triple1) -> rule1)) -> rule5))] @1: The cat is rough.[(((triple1) -> rule4))] @2: The cat is round.[(((((triple1) -> rule4) triple1) -> rule1))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat is not nice.
("cat" "is" "nice" "-")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
((((((triple1) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2