The cat is round. Nice people are young. All rough, nice people are young. If someone is round then they are young. If someone is rough then they are nice. If someone is round then they are rough. All green people are rough. Nice people are round. All rough, nice people are not green.
The cat is round.
("cat" "is" "round" "+")
Nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
All rough, nice people are young.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is rough then they are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
All rough, nice people are not green.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "-"))
The cat is round.
True
1
proof
[(triple1)]
("cat" "is" "round" "+")
triple1
The cat is not round.
False
1
inv-proof
[(triple1)]
("cat" "is" "round" "-")
triple1
The cat is rough.
True
2
proof
[(((triple1) -> rule5))]
("cat" "is" "rough" "+")
((triple1) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is not rough.
False
2
inv-proof
[(((triple1) -> rule5))]
("cat" "is" "rough" "-")
((triple1) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is nice.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("cat" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is not nice.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("cat" "is" "nice" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is not green.
True
6
proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule4)) -> rule8))]
("cat" "is" "green" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is green.
False
6
inv-proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule4)) -> rule8))]
("cat" "is" "green" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
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 visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is round.[(triple1)] @1: The cat is rough.[(((triple1) -> rule5))] The cat is young.[(((triple1) -> rule3) OR ((((((triple1) -> rule5)) -> rule4)) -> rule1) OR ((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule4)) -> rule2))] @2: The cat is nice.[(((((triple1) -> rule5)) -> rule4))] @3: The cat is not green.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule4)) -> rule8))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
((triple1) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((triple1) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is not green.
("cat" "is" "green" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3