Bob is big. Bob is blue. Bob is not kind. Bob is quiet. Bob is red. Bob is round. Bob is young. Gary is big. Gary is blue. Gary is kind. Gary is red. Gary is round. Gary is young. Harry is not big. Harry is blue. Harry is red. If Harry is red then Harry is not young. If someone is kind and not young then they are round.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is red.
("Harry" "is" "red" "+")
If Harry is red then Harry is not young.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "young" "-"))
If someone is kind and not young then they are round.
((("someone" "is" "kind" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "round" "+"))
Gary is big.
True
1
proof
[(triple8)]
("Gary" "is" "big" "+")
triple8
Bob is not quiet.
False
1
inv-proof
[(triple4)]
("Bob" "is" "quiet" "-")
triple4
Harry is not young.
True
2
proof
[(((triple16) -> rule1))]
("Harry" "is" "young" "-")
((triple16) -> (rule1 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is young.
False
2
inv-proof
[(((triple16) -> rule1))]
("Harry" "is" "young" "+")
((triple16) -> (rule1 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "round" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is not kind.[(triple3)] Bob is quiet.[(triple4)] Bob is red.[(triple5)] Bob is round.[(triple6)] Bob is young.[(triple7)] Gary is big.[(triple8)] Gary is blue.[(triple9)] Gary is kind.[(triple10)] Gary is red.[(triple11)] Gary is round.[(triple12)] Gary is young.[(triple13)] Harry is blue.[(triple15)] Harry is not big.[(triple14)] Harry is red.[(triple16)] @1: Harry is not young.[(((triple16) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is not kind.
("Bob" "is" "kind" "-")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
Gary is young.
("Gary" "is" "young" "+")
triple13
Harry is blue.
("Harry" "is" "blue" "+")
triple15
Harry is not big.
("Harry" "is" "big" "-")
triple14
Harry is red.
("Harry" "is" "red" "+")
triple16
Harry is not young.
("Harry" "is" "young" "-")
((triple16) -> (rule1 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1