Dave is big. Dave is green. Dave is kind. Dave is nice. Dave is rough. Harry is furry. Harry is green. All nice, furry people are big. All big people are rough. Kind people are rough. If Harry is furry then Harry is nice. All kind people are big. All green, big people are rough.
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
All nice, furry people are big.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If Harry is furry then Harry is nice.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "nice" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
All green, big people are rough.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Dave is rough.
True
1
proof
[(triple5 OR ((triple1) -> rule2) OR ((triple3) -> rule3) OR ((triple2 triple1) -> rule6) OR ((((triple3) -> rule5)) -> rule2) OR ((triple2 ((triple3) -> rule5)) -> rule6))]
("Dave" "is" "rough" "+")
triple5
((triple1) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple3) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple2 triple1) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple2 ((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Harry is nice.
True
2
proof
[(((triple6) -> rule4))]
("Harry" "is" "nice" "+")
((triple6) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple6) -> rule4))]
("Harry" "is" "nice" "-")
((triple6) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
True
4
proof
[(((((triple6) -> rule4) triple6) -> rule1))]
("Harry" "is" "big" "+")
((((triple6) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not big.
False
4
inv-proof
[(((((triple6) -> rule4) triple6) -> rule1))]
("Harry" "is" "big" "-")
((((triple6) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Dave is big.[(triple1 OR ((triple3) -> rule5))] Dave is green.[(triple2)] Dave is kind.[(triple3)] Dave is nice.[(triple4)] Dave is rough.[(triple5 OR ((triple1) -> rule2) OR ((triple3) -> rule3) OR ((triple2 triple1) -> rule6) OR ((((triple3) -> rule5)) -> rule2) OR ((triple2 ((triple3) -> rule5)) -> rule6))] Harry is furry.[(triple6)] Harry is green.[(triple7)] @1: Harry is nice.[(((triple6) -> rule4))] @2: Harry is big.[(((((triple6) -> rule4) triple6) -> rule1))] @3: Harry is rough.[(((((((triple6) -> rule4) triple6) -> rule1)) -> rule2) OR ((triple7 ((((triple6) -> rule4) triple6) -> rule1)) -> rule6))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple3) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple1) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple3) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple2 triple1) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple2 ((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
((triple6) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple6) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple6) -> (rule4 % int3)) triple6) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((triple7 ((((triple6) -> (rule4 % int3)) triple6) -> (rule1 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3