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