Anne is nice. Anne is smart. Anne is young. Bob is nice. Bob is white. Charlie is white. Charlie is young. White things are smart. All young, nice things are smart. If Bob is smart and Bob is nice then Bob is blue.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
White things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
All young, nice things are smart.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Bob is smart and Bob is nice then Bob is blue.
((("Bob" "is" "smart" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "blue" "+"))
Anne is young.
True
1
proof
[(triple3)]
("Anne" "is" "young" "+")
triple3
Bob is not nice.
False
1
inv-proof
[(triple4)]
("Bob" "is" "nice" "-")
triple4
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is nice.[(triple1)] Anne is smart.[(triple2 OR ((triple3 triple1) -> rule2))] Anne is young.[(triple3)] Bob is nice.[(triple4)] Bob is white.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7)] @1: Bob is smart.[(((triple5) -> rule1))] Charlie is smart.[(((triple6) -> rule1))] @2: Bob is blue.[(((((triple5) -> rule1) triple4) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
((triple3 triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple5) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple6) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple5) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2