Anne is smart. Bob is smart. Charlie is blue. Gary is round. If something is smart and kind then it is young. If something is blue and kind then it is cold. If Gary is kind then Gary is blue. If something is cold then it is kind. If something is quiet then it is smart. If Bob is smart and Bob is kind then Bob is cold. If Anne is young and Anne is blue then Anne is cold. Smart things are young.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is smart and kind then it is young.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is blue and kind then it is cold.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If Gary is kind then Gary is blue.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "blue" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If Bob is smart and Bob is kind then Bob is cold.
((("Bob" "is" "smart" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "cold" "+"))
If Anne is young and Anne is blue then Anne is cold.
((("Anne" "is" "young" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "cold" "+"))
Smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Bob is smart.
True
1
proof
[(triple2)]
("Bob" "is" "smart" "+")
triple2
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Anne is young.
True
2
proof
[(((triple1) -> rule8))]
("Anne" "is" "young" "+")
((triple1) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple2) -> rule8))]
("Bob" "is" "young" "-")
((triple2) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is not blue.
Unknown
inv-rconc
[@3: Gary is blue.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule2 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is kind.
Unknown
rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Gary" "is" "kind" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is smart.[(triple1)] Bob is smart.[(triple2)] Charlie is blue.[(triple3)] Gary is round.[(triple4)] @1: Anne is young.[(((triple1) -> rule8))] Bob is young.[(((triple2) -> rule8))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1