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