The cat is not big. The cat is not cold. The cat is nice. All big, round people are nice. If the cat is big and the cat is nice then the cat is cold. If someone is nice and not big then they are round. All big people are round. Cold, big people are young. If the cat is round then the cat is young.
The cat is not big.
("cat" "is" "big" "-")
The cat is not cold.
("cat" "is" "cold" "-")
The cat is nice.
("cat" "is" "nice" "+")
All big, round people are nice.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If the cat is big and the cat is nice then the cat is cold.
((("cat" "is" "big" "+") ("cat" "is" "nice" "+")) -> ("cat" "is" "cold" "+"))
If someone is nice and not big then they are round.
((("someone" "is" "nice" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "round" "+"))
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Cold, big people are young.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If the cat is round then the cat is young.
((("cat" "is" "round" "+")) -> ("cat" "is" "young" "+"))
The cat is not big.
True
1
proof
[(triple1)]
("cat" "is" "big" "-")
triple1
The cat is big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The cat is round.
True
3
proof
[(((triple3 triple1) -> rule3))]
("cat" "is" "round" "+")
((triple3 triple1) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is not round.
False
3
inv-proof
[(((triple3 triple1) -> rule3))]
("cat" "is" "round" "-")
((triple3 triple1) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is young.
True
4
proof
[(((((triple3 triple1) -> rule3)) -> rule6))]
("cat" "is" "young" "+")
((((triple3 triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is not young.
False
4
inv-proof
[(((((triple3 triple1) -> rule3)) -> rule6))]
("cat" "is" "young" "-")
((((triple3 triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
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 visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is nice.[(triple3)] The cat is not big.[(triple1)] The cat is not cold.[(triple2)] @1: The cat is round.[(((triple3 triple1) -> rule3))] @2: The cat is young.[(((((triple3 triple1) -> rule3)) -> rule6))]
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is not big.
("cat" "is" "big" "-")
triple1
The cat is not cold.
("cat" "is" "cold" "-")
triple2
The cat is round.
("cat" "is" "round" "+")
((triple3 triple1) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((((triple3 triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2