Anne is blue. Anne is green. Anne is kind. Anne is white. Anne is young. Dave is green. Dave is young. Gary is green. Gary is round. Gary is white. If Anne is white and Anne is blue then Anne is young. If Gary is white and Gary is young then Gary is kind. All young, white people are round.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If Anne is white and Anne is blue then Anne is young.
((("Anne" "is" "white" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "young" "+"))
If Gary is white and Gary is young then Gary is kind.
((("Gary" "is" "white" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "kind" "+"))
All young, white people are round.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Anne is young.
True
1
proof
[(triple5 OR ((triple4 triple1) -> rule1))]
("Anne" "is" "young" "+")
triple5
((triple4 triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is not green.
False
1
inv-proof
[(triple6)]
("Dave" "is" "green" "-")
triple6
Anne is round.
True
3
proof
[(((triple5 triple4) -> rule3) OR ((((triple4 triple1) -> rule1) triple4) -> rule3))]
("Anne" "is" "round" "+")
((triple5 triple4) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple4 triple1) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not round.
False
3
inv-proof
[(((triple5 triple4) -> rule3) OR ((((triple4 triple1) -> rule1) triple4) -> rule3))]
("Anne" "is" "round" "-")
((triple5 triple4) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple4 triple1) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "kind" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is kind.[(triple3)] Anne is white.[(triple4)] Anne is young.[(triple5 OR ((triple4 triple1) -> rule1))] Dave is green.[(triple6)] Dave is young.[(triple7)] Gary is green.[(triple8)] Gary is round.[(triple9)] Gary is white.[(triple10)] @1: Anne is round.[(((triple5 triple4) -> rule3) OR ((((triple4 triple1) -> rule1) triple4) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
((triple4 triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Anne is round.
("Anne" "is" "round" "+")
((triple5 triple4) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple4 triple1) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2