Bob is not big. Bob is furry. Bob is kind. Bob is not round. Bob is not young. Gary is big. Gary is not blue. Gary is furry. Gary is kind. Gary is red. Gary is round. Gary is young. Harry is not blue. Harry is kind. Harry is round. Red people are big. If someone is blue and not furry then they are not big. All blue, big people are kind. If Gary is kind then Gary is not blue. All blue people are red. All round people are red.
Bob is not big.
("Bob" "is" "big" "-")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is not young.
("Bob" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is furry.
("Gary" "is" "furry" "+")
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 blue.
("Harry" "is" "blue" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is blue and not furry then they are not big.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "big" "-"))
All blue, big people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If Gary is kind then Gary is not blue.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "blue" "-"))
All blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
All round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Bob is kind.
True
1
proof
[(triple3)]
("Bob" "is" "kind" "+")
triple3
Gary is not kind.
False
1
inv-proof
[(triple9)]
("Gary" "is" "kind" "-")
triple9
Harry is red.
True
2
proof
[(((triple15) -> rule6))]
("Harry" "is" "red" "+")
((triple15) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple15) -> rule6))]
("Harry" "is" "red" "-")
((triple15) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is furry.[(triple2)] Bob is kind.[(triple3)] Bob is not big.[(triple1)] Bob is not round.[(triple4)] Bob is not young.[(triple5)] Gary is big.[(triple6 OR ((triple10) -> rule1) OR ((((triple11) -> rule6)) -> rule1))] Gary is furry.[(triple8)] Gary is kind.[(triple9)] Gary is not blue.[(triple7 OR ((triple9) -> rule4))] Gary is red.[(triple10 OR ((triple11) -> rule6))] Gary is round.[(triple11)] Gary is young.[(triple12)] Harry is kind.[(triple14)] Harry is not blue.[(triple13)] Harry is round.[(triple15)] @1: Harry is red.[(((triple15) -> rule6))] @2: Harry is big.[(((((triple15) -> rule6)) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is not round.
("Bob" "is" "round" "-")
triple4
Bob is not young.
("Bob" "is" "young" "-")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
((triple10) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple11) -> (rule6 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is not blue.
("Gary" "is" "blue" "-")
triple7
((triple9) -> (rule4 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
triple10
((triple11) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is not blue.
("Harry" "is" "blue" "-")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is red.
("Harry" "is" "red" "+")
((triple15) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple15) -> (rule6 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2