The cat is kind. The cat is not nice. The cat is red. The cat is rough. The cat is round. If the cat is rough and the cat is not kind then the cat is red. Red people are rough. Kind, nice people are rough. Rough people are round. If the cat is rough then the cat is round. If someone is rough then they are not nice.
The cat is kind.
("cat" "is" "kind" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
If the cat is rough and the cat is not kind then the cat is red.
((("cat" "is" "rough" "+") ("cat" "is" "kind" "~")) -> ("cat" "is" "red" "+"))
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Kind, nice people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If the cat is rough then the cat is round.
((("cat" "is" "rough" "+")) -> ("cat" "is" "round" "+"))
If someone is rough then they are not nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "-"))
The cat is round.
True
1
proof
[(triple5 OR ((triple4) -> rule4) OR ((triple4) -> rule5) OR ((((triple3) -> rule2)) -> rule4) OR ((((triple3) -> rule2)) -> rule5))]
("cat" "is" "round" "+")
triple5
((triple4) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple4) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is not rough.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule2))]
("cat" "is" "rough" "-")
triple4
((triple3) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat is kind.[(triple1)] The cat is not nice.[(triple2 OR ((triple4) -> rule6) OR ((((triple3) -> rule2)) -> rule6))] The cat is red.[(triple3)] The cat is rough.[(triple4 OR ((triple3) -> rule2))] The cat is round.[(triple5 OR ((triple4) -> rule4) OR ((triple4) -> rule5) OR ((((triple3) -> rule2)) -> rule4) OR ((((triple3) -> rule2)) -> rule5))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat is not nice.
("cat" "is" "nice" "-")
triple2
((triple4) -> (rule6 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
((triple3) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is round.
("cat" "is" "round" "+")
triple5
((triple4) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple4) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2