The cat is young. Blue, green things are nice. If something is blue and green then it is nice. If something is rough then it is blue. All young things are rough. If the cat is nice and the cat is green then the cat is blue. If the cat is young and the cat is rough then the cat is green.
The cat is young.
("cat" "is" "young" "+")
Blue, green things are nice.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is blue and green then it is nice.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it is blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If the cat is nice and the cat is green then the cat is blue.
((("cat" "is" "nice" "+") ("cat" "is" "green" "+")) -> ("cat" "is" "blue" "+"))
If the cat is young and the cat is rough then the cat is green.
((("cat" "is" "young" "+") ("cat" "is" "rough" "+")) -> ("cat" "is" "green" "+"))
The cat is young.
True
1
proof
[(triple1)]
("cat" "is" "young" "+")
triple1
The cat is not young.
False
1
inv-proof
[(triple1)]
("cat" "is" "young" "-")
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 is blue.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("cat" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is not blue.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("cat" "is" "blue" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is nice.
True
8
proof
[(((((((triple1) -> rule4)) -> rule3) ((triple1 ((triple1) -> rule4)) -> rule6)) -> rule1) OR ((((((triple1) -> rule4)) -> rule3) ((triple1 ((triple1) -> rule4)) -> rule6)) -> rule2))]
("cat" "is" "nice" "+")
((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The cat is not nice.
False
8
inv-proof
[(((((((triple1) -> rule4)) -> rule3) ((triple1 ((triple1) -> rule4)) -> rule6)) -> rule1) OR ((((((triple1) -> rule4)) -> rule3) ((triple1 ((triple1) -> rule4)) -> rule6)) -> rule2))]
("cat" "is" "nice" "-")
((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "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 young.[(triple1)] @1: The cat is rough.[(((triple1) -> rule4))] @2: The cat is blue.[(((((triple1) -> rule4)) -> rule3))] The cat is green.[(((triple1 ((triple1) -> rule4)) -> rule6))] @3: The cat is nice.[(((((((triple1) -> rule4)) -> rule3) ((triple1 ((triple1) -> rule4)) -> rule6)) -> rule1) OR ((((((triple1) -> rule4)) -> rule3) ((triple1 ((triple1) -> rule4)) -> rule6)) -> rule2))]
The cat is young.
("cat" "is" "young" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is green.
("cat" "is" "green" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4
((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
int4