Dave is kind. Kind people are smart. If someone is quiet then they are smart. If Dave is not quiet then Dave is round. Round people are white. All big people are round. If Dave is smart then Dave is big.
Dave is kind.
("Dave" "is" "kind" "+")
Kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet then they are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If Dave is not quiet then Dave is round.
((("Dave" "is" "quiet" "~")) -> ("Dave" "is" "round" "+"))
Round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If Dave is smart then Dave is big.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "big" "+"))
Dave is kind.
True
1
proof
[(triple1)]
("Dave" "is" "kind" "+")
triple1
Dave is not kind.
False
1
inv-proof
[(triple1)]
("Dave" "is" "kind" "-")
triple1
Dave is smart.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("Dave" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("Dave" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Dave is kind.[(triple1)] @1: Dave is smart.[(((triple1) -> rule1))] @2: Dave is big.[(((((triple1) -> rule1)) -> rule6))] @3: Dave is round.[(((((((triple1) -> rule1)) -> rule6)) -> rule5))] @4: Dave is white.[(((((((((triple1) -> rule1)) -> rule6)) -> rule5)) -> rule4))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4