Anne is green. Anne is nice. Dave is blue. Dave is rough. Gary is big. Gary is nice. Harry is nice. Round, rough things are nice. If something is nice and round then it is big. If Anne is big and Anne is rough then Anne is nice. If something is nice then it is big. If something is rough and kind then it is nice. All big, nice things are round. All kind, big things are nice. If Dave is rough then Dave is blue.
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Round, rough things are nice.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is nice and round then it is big.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Anne is big and Anne is rough then Anne is nice.
((("Anne" "is" "big" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "nice" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is rough and kind then it is nice.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All big, nice things are round.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All kind, big things are nice.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If Dave is rough then Dave is blue.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "blue" "+"))
Gary is nice.
True
1
proof
[(triple6)]
("Gary" "is" "nice" "+")
triple6
Harry is not nice.
False
1
inv-proof
[(triple7)]
("Harry" "is" "nice" "-")
triple7
Dave is not big.
Unknown
inv-rconc
[@4: Dave is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule6 <- rule2 <- FAIL)]]
("Dave" "is" "big" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is green.[(triple1)] Anne is nice.[(triple2)] Dave is blue.[(triple3 OR ((triple4) -> rule8))] Dave is rough.[(triple4)] Gary is big.[(triple5 OR ((triple6) -> rule4))] Gary is nice.[(triple6)] Harry is nice.[(triple7)] @1: Anne is big.[(((triple2) -> rule4))] Gary is round.[(((triple5 triple6) -> rule6) OR ((((triple6) -> rule4) triple6) -> rule6))] Harry is big.[(((triple7) -> rule4))] @2: Anne is round.[(((((triple2) -> rule4) triple2) -> rule6))] Harry is round.[(((((triple7) -> rule4) triple7) -> rule6))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
((triple4) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
((triple6) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple5 triple6) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple6) -> (rule4 % int2)) triple6) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((triple7) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple7) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2