The cat is blue. The cat is green. The cat is kind. The cat is red. The cat is rough. All rough things are red. If something is red then it is green. All blue things are kind. If something is blue then it is rough. All blue things are green. If the cat is green then the cat is kind.
The cat is blue.
("cat" "is" "blue" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
All rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If the cat is green then the cat is kind.
((("cat" "is" "green" "+")) -> ("cat" "is" "kind" "+"))
The cat is red.
True
1
proof
[(triple4 OR ((triple5) -> rule1) OR ((((triple1) -> rule4)) -> rule1))]
("cat" "is" "red" "+")
triple4
((triple5) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is not blue.
False
1
inv-proof
[(triple1)]
("cat" "is" "blue" "-")
triple1
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is blue.[(triple1)] The cat is green.[(triple2 OR ((triple1) -> rule5) OR ((triple4) -> rule2) OR ((((triple5) -> rule1)) -> rule2) OR ((((((triple1) -> rule4)) -> rule1)) -> rule2))] The cat is kind.[(triple3 OR ((triple1) -> rule3) OR ((triple2) -> rule6) OR ((((triple1) -> rule5)) -> rule6) OR ((((triple4) -> rule2)) -> rule6) OR ((((((triple5) -> rule1)) -> rule2)) -> rule6) OR ((((((((triple1) -> rule4)) -> rule1)) -> rule2)) -> rule6))] The cat is red.[(triple4 OR ((triple5) -> rule1) OR ((((triple1) -> rule4)) -> rule1))] The cat is rough.[(triple5 OR ((triple1) -> rule4))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
((triple1) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
((triple4) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
triple3
((triple1) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple2) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
((((((((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The cat is red.
("cat" "is" "red" "+")
triple4
((triple5) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
triple5
((triple1) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1