The cow is round. If the cow is rough and the cow is not round then the cow is not big. If the cow is rough then the cow is big. If the cow is young then the cow is rough. Round people are nice. If the cow is big then the cow is young. Round people are big.
The cow is round.
("cow" "is" "round" "+")
If the cow is rough and the cow is not round then the cow is not big.
((("cow" "is" "rough" "+") ("cow" "is" "round" "~")) -> ("cow" "is" "big" "-"))
If the cow is rough then the cow is big.
((("cow" "is" "rough" "+")) -> ("cow" "is" "big" "+"))
If the cow is young then the cow is rough.
((("cow" "is" "young" "+")) -> ("cow" "is" "rough" "+"))
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If the cow is big then the cow is young.
((("cow" "is" "big" "+")) -> ("cow" "is" "young" "+"))
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
The cow is round.
True
1
proof
[(triple1)]
("cow" "is" "round" "+")
triple1
The cow is not round.
False
1
inv-proof
[(triple1)]
("cow" "is" "round" "-")
triple1
The cow is nice.
True
2
proof
[(((triple1) -> rule4))]
("cow" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("cow" "is" "nice" "-")
((triple1) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is young.
True
3
proof
[(((((triple1) -> rule6)) -> rule5))]
("cow" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is not young.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5))]
("cow" "is" "young" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is rough.
True
4
proof
[(((((((triple1) -> rule6)) -> rule5)) -> rule3))]
("cow" "is" "rough" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is not rough.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule5)) -> rule3))]
("cow" "is" "rough" "-")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cow is round.[(triple1)] @1: The cow is big.[(((triple1) -> rule6))] The cow is nice.[(((triple1) -> rule4))] @2: The cow is young.[(((((triple1) -> rule6)) -> rule5))] @3: The cow is rough.[(((((((triple1) -> rule6)) -> rule5)) -> rule3))]
The cow is round.
("cow" "is" "round" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
((triple1) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3