The cat is big. If the cat is round and the cat is big then the cat is rough. All big people are young. Big people are round.
The cat is big.
("cat" "is" "big" "+")
If the cat is round and the cat is big then the cat is rough.
((("cat" "is" "round" "+") ("cat" "is" "big" "+")) -> ("cat" "is" "rough" "+"))
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
The cat is big.
True
1
proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The cat is not big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "-")
triple1
The cat is round.
True
2
proof
[(((triple1) -> rule3))]
("cat" "is" "round" "+")
((triple1) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is not young.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "is" "young" "-")
((triple1) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("cat" "is" "rough" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is not rough.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("cat" "is" "rough" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat is big.[(triple1)] @1: The cat is round.[(((triple1) -> rule3))] The cat is young.[(((triple1) -> rule2))] @2: The cat is rough.[(((((triple1) -> rule3) triple1) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
((triple1) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((triple1) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2