Bob is big. Bob is furry. Bob is nice. Bob is not red. Bob is rough. Bob is young. Gary is big. Gary is blue. Gary is furry. Gary is nice. Gary is red. Gary is rough. Gary is young. Harry is furry. Harry is nice. If Gary is young then Gary is blue. All furry things are big. All nice things are big. If something is blue and not nice then it is red. If Bob is not big and Bob is not nice then Bob is blue. If Bob is young and Bob is not big then Bob is not red.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If Gary is young then Gary is blue.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "blue" "+"))
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is blue and not nice then it is red.
((("something" "is" "blue" "+") ("something" "is" "nice" "~")) -> ("something" "is" "red" "+"))
If Bob is not big and Bob is not nice then Bob is blue.
((("Bob" "is" "big" "~") ("Bob" "is" "nice" "~")) -> ("Bob" "is" "blue" "+"))
If Bob is young and Bob is not big then Bob is not red.
((("Bob" "is" "young" "+") ("Bob" "is" "big" "~")) -> ("Bob" "is" "red" "-"))
Gary is big.
True
1
proof
[(triple7 OR ((triple10) -> rule3) OR ((triple9) -> rule2))]
("Gary" "is" "big" "+")
triple7
((triple10) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple9) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is not young.
False
1
inv-proof
[(triple6)]
("Bob" "is" "young" "-")
triple6
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "blue" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is big.[(triple1 OR ((triple2) -> rule2) OR ((triple3) -> rule3))] Bob is furry.[(triple2)] Bob is nice.[(triple3)] Bob is not red.[(triple4)] Bob is rough.[(triple5)] Bob is young.[(triple6)] Gary is big.[(triple7 OR ((triple10) -> rule3) OR ((triple9) -> rule2))] Gary is blue.[(triple8 OR ((triple13) -> rule1))] Gary is furry.[(triple9)] Gary is nice.[(triple10)] Gary is red.[(triple11)] Gary is rough.[(triple12)] Gary is young.[(triple13)] Harry is furry.[(triple14)] Harry is nice.[(triple15)] @1: Harry is big.[(((triple14) -> rule2) OR ((triple15) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple3) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not red.
("Bob" "is" "red" "-")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
((triple10) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple9) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple8
((triple13) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Gary is young.
("Gary" "is" "young" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
Harry is nice.
("Harry" "is" "nice" "+")
triple15
Harry is big.
("Harry" "is" "big" "+")
((triple14) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple15) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1