The cat is blue. The cat is green. The cat is kind. The cat is not nice. The cat is rough. Blue, kind things are not nice. Rough things are blue. If something is blue and nice then it is rough. If the cat is not rough then the cat is green. If the cat is blue then the cat is green. If the cat is not kind then the cat is green.
The cat is blue.
("cat" "is" "blue" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat is rough.
("cat" "is" "rough" "+")
Blue, kind things are not nice.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "-"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is blue and nice then it is rough.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If the cat is not rough then the cat is green.
((("cat" "is" "rough" "~")) -> ("cat" "is" "green" "+"))
If the cat is blue then the cat is green.
((("cat" "is" "blue" "+")) -> ("cat" "is" "green" "+"))
If the cat is not kind then the cat is green.
((("cat" "is" "kind" "~")) -> ("cat" "is" "green" "+"))
The cat is not nice.
True
1
proof
[(triple4 OR ((triple1 triple3) -> rule1) OR ((((triple5) -> rule2) triple3) -> rule1))]
("cat" "is" "nice" "-")
triple4
((triple1 triple3) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
((((triple5) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is nice.
False
1
inv-proof
[(triple4 OR ((triple1 triple3) -> rule1) OR ((((triple5) -> rule2) triple3) -> rule1))]
("cat" "is" "nice" "+")
triple4
((triple1 triple3) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
((((triple5) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat is blue.[(triple1 OR ((triple5) -> rule2))] The cat is green.[(triple2 OR ((triple1) -> rule5) OR ((((triple5) -> rule2)) -> rule5))] The cat is kind.[(triple3)] The cat is not nice.[(triple4 OR ((triple1 triple3) -> rule1) OR ((((triple5) -> rule2) triple3) -> rule1))] The cat is rough.[(triple5)]
The cat is blue.
("cat" "is" "blue" "+")
triple1
((triple5) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is green.
("cat" "is" "green" "+")
triple2
((triple1) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is not nice.
("cat" "is" "nice" "-")
triple4
((triple1 triple3) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
((((triple5) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
triple5