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