Bob is big. Bob is green. Bob is kind. Bob is quiet. Bob is round. Gary is big. Gary is round. Harry is big. Harry is round. Harry is white. If something is kind then it is furry. Round things are kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is kind then it is furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple9)]
("Harry" "is" "round" "-")
triple9
Gary is kind.
True
2
proof
[(((triple7) -> rule2))]
("Gary" "is" "kind" "+")
((triple7) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple7) -> rule2))]
("Gary" "is" "kind" "-")
((triple7) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("Gary" "is" "furry" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule1))]
("Harry" "is" "furry" "-")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3 OR ((triple5) -> rule2))] Bob is quiet.[(triple4)] Bob is round.[(triple5)] Gary is big.[(triple6)] Gary is round.[(triple7)] Harry is big.[(triple8)] Harry is round.[(triple9)] Harry is white.[(triple10)] @1: Bob is furry.[(((triple3) -> rule1) OR ((((triple5) -> rule2)) -> rule1))] Gary is kind.[(((triple7) -> rule2))] Harry is kind.[(((triple9) -> rule2))] @2: Gary is furry.[(((((triple7) -> rule2)) -> rule1))] Harry is furry.[(((((triple9) -> rule2)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple5) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Bob is furry.
("Bob" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((triple7) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple9) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2