Dave is kind. Dave is round. Dave is young. Harry is big. Harry is quiet. Harry is round. Harry is young. If something is kind then it is big.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is kind then it is big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Dave is young.
True
1
proof
[(triple3)]
("Dave" "is" "young" "+")
triple3
Harry is not round.
False
1
inv-proof
[(triple6)]
("Harry" "is" "round" "-")
triple6
Dave is big.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "big" "+")
((triple1) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "big" "-")
((triple1) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Dave is kind.[(triple1)] Dave is round.[(triple2)] Dave is young.[(triple3)] Harry is big.[(triple4)] Harry is quiet.[(triple5)] Harry is round.[(triple6)] Harry is young.[(triple7)] @1: Dave is big.[(((triple1) -> rule1))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
((triple1) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1