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