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