Anne is big. Anne is green. Anne is smart. Anne is young. Dave is big. Dave is blue. Dave is white. Dave is young. Gary is big. Gary is blue. Gary is green. Gary is kind. Gary is smart. Gary is white. Gary is young. If Gary is not smart and Gary is not white then Gary is not blue. Kind things are blue. Smart, white things are blue. All white things are kind. If something is smart and not white then it is big. All kind things are young.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is not smart and Gary is not white then Gary is not blue.
((("Gary" "is" "smart" "~") ("Gary" "is" "white" "~")) -> ("Gary" "is" "blue" "-"))
Kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Smart, white things are blue.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
All white things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is smart and not white then it is big.
((("something" "is" "smart" "+") ("something" "is" "white" "~")) -> ("something" "is" "big" "+"))
All kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Gary is big.
True
1
proof
[(triple9)]
("Gary" "is" "big" "+")
triple9
Anne is not smart.
False
1
inv-proof
[(triple3)]
("Anne" "is" "smart" "-")
triple3
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Anne is smart.[(triple3)] Anne is young.[(triple4)] Dave is big.[(triple5)] Dave is blue.[(triple6 OR ((((triple7) -> rule4)) -> rule2))] Dave is white.[(triple7)] Dave is young.[(triple8 OR ((((triple7) -> rule4)) -> rule6))] Gary is big.[(triple9)] Gary is blue.[(triple10 OR ((triple12) -> rule2) OR ((triple13 triple14) -> rule3) OR ((((triple14) -> rule4)) -> rule2))] Gary is green.[(triple11)] Gary is kind.[(triple12 OR ((triple14) -> rule4))] Gary is smart.[(triple13)] Gary is white.[(triple14)] Gary is young.[(triple15 OR ((triple12) -> rule6) OR ((((triple14) -> rule4)) -> rule6))] @1: Dave is kind.[(((triple7) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is blue.
("Gary" "is" "blue" "+")
triple10
((triple12) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple13 triple14) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple14) -> (rule4 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple11
Gary is kind.
("Gary" "is" "kind" "+")
triple12
((triple14) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Gary is white.
("Gary" "is" "white" "+")
triple14
Gary is young.
("Gary" "is" "young" "+")
triple15
((triple12) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple14) -> (rule4 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((triple7) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1