Dave is quiet. Dave is smart. Dave is white. Dave is young. Gary is furry. Gary is kind. Gary is rough. Gary is white. Gary is young. Harry is furry. Harry is kind. Harry is quiet. Harry is rough. Harry is smart. Harry is white. Harry is young. Young things are furry. Furry things are kind. Kind things are smart.
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
Young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Gary is furry.
True
1
proof
[(triple5 OR ((triple9) -> rule1))]
("Gary" "is" "furry" "+")
triple5
((triple9) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Dave is not quiet.
False
1
inv-proof
[(triple1)]
("Dave" "is" "quiet" "-")
triple1
Dave is furry.
True
2
proof
[(((triple4) -> rule1))]
("Dave" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple4) -> rule1))]
("Dave" "is" "furry" "-")
((triple4) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Dave" "is" "kind" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Dave" "is" "kind" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is quiet.[(triple1)] Dave is smart.[(triple2 OR ((((((triple4) -> rule1)) -> rule2)) -> rule3))] Dave is white.[(triple3)] Dave is young.[(triple4)] Gary is furry.[(triple5 OR ((triple9) -> rule1))] Gary is kind.[(triple6 OR ((triple5) -> rule2) OR ((((triple9) -> rule1)) -> rule2))] Gary is rough.[(triple7)] Gary is white.[(triple8)] Gary is young.[(triple9)] Harry is furry.[(triple10 OR ((triple16) -> rule1))] Harry is kind.[(triple11 OR ((triple10) -> rule2) OR ((((triple16) -> rule1)) -> rule2))] Harry is quiet.[(triple12)] Harry is rough.[(triple13)] Harry is smart.[(triple14 OR ((triple11) -> rule3) OR ((((triple10) -> rule2)) -> rule3) OR ((((((triple16) -> rule1)) -> rule2)) -> rule3))] Harry is white.[(triple15)] Harry is young.[(triple16)] @1: Dave is furry.[(((triple4) -> rule1))] Gary is smart.[(((triple6) -> rule3) OR ((((triple5) -> rule2)) -> rule3) OR ((((((triple9) -> rule1)) -> rule2)) -> rule3))] @2: Dave is kind.[(((((triple4) -> rule1)) -> rule2))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
((triple9) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple6
((triple5) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Gary is white.
("Gary" "is" "white" "+")
triple8
Gary is young.
("Gary" "is" "young" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
((triple16) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple11
((triple10) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple16) -> (rule1 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
((triple11) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((triple16) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Dave is furry.
("Dave" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple6) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2