The cat is nice. If someone is nice and blue then they are kind. All round, nice people are kind. If someone is round then they are blue. If the cat is round then the cat is blue. If the cat is blue and the cat is nice then the cat is red. Nice, blue people are round. All round people are nice. Nice people are round.
The cat is nice.
("cat" "is" "nice" "+")
If someone is nice and blue then they are kind.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All round, nice people are kind.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If the cat is round then the cat is blue.
((("cat" "is" "round" "+")) -> ("cat" "is" "blue" "+"))
If the cat is blue and the cat is nice then the cat is red.
((("cat" "is" "blue" "+") ("cat" "is" "nice" "+")) -> ("cat" "is" "red" "+"))
Nice, blue people are round.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
The cat is nice.
True
1
proof
[(triple1)]
("cat" "is" "nice" "+")
triple1
The cat is not nice.
False
1
inv-proof
[(triple1)]
("cat" "is" "nice" "-")
triple1
The cat is round.
True
2
proof
[(((triple1) -> rule8))]
("cat" "is" "round" "+")
((triple1) -> (rule8 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is not round.
False
2
inv-proof
[(((triple1) -> rule8))]
("cat" "is" "round" "-")
((triple1) -> (rule8 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is blue.
True
3
proof
[(((((triple1) -> rule8)) -> rule3) OR ((((triple1) -> rule8)) -> rule4))]
("cat" "is" "blue" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is not blue.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule3) OR ((((triple1) -> rule8)) -> rule4))]
("cat" "is" "blue" "-")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
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 nice.[(triple1)] @1: The cat is round.[(((triple1) -> rule8))] @2: The cat is blue.[(((((triple1) -> rule8)) -> rule3) OR ((((triple1) -> rule8)) -> rule4))] The cat is kind.[(((((triple1) -> rule8) triple1) -> rule2) OR ((triple1 ((((triple1) -> rule8)) -> rule3)) -> rule1) OR ((triple1 ((((triple1) -> rule8)) -> rule4)) -> rule1))] @3: The cat is red.[(((((((triple1) -> rule8)) -> rule3) triple1) -> rule5) OR ((((((triple1) -> rule8)) -> rule4) triple1) -> rule5))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
((triple1) -> (rule8 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat is red.
("cat" "is" "red" "+")
((((((triple1) -> (rule8 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3