Anne is blue. Anne is cold. Anne is smart. Charlie is quiet. Dave is cold. Dave is nice. Dave is quiet. Dave is smart. Gary is blue. Gary is young. If something is smart then it is nice. Cold things are quiet. Nice things are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Dave is cold.
True
1
proof
[(triple5)]
("Dave" "is" "cold" "+")
triple5
Anne is not smart.
False
1
inv-proof
[(triple3)]
("Anne" "is" "smart" "-")
triple3
Anne is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Anne" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple6) -> rule3) OR ((((triple8) -> rule1)) -> rule3))]
("Dave" "is" "blue" "-")
((triple6) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Charlie is not blue.
Unknown
inv-rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Anne is blue.[(triple1 OR ((((triple3) -> rule1)) -> rule3))] Anne is cold.[(triple2)] Anne is smart.[(triple3)] Charlie is quiet.[(triple4)] Dave is cold.[(triple5)] Dave is nice.[(triple6 OR ((triple8) -> rule1))] Dave is quiet.[(triple7 OR ((triple5) -> rule2))] Dave is smart.[(triple8)] Gary is blue.[(triple9)] Gary is young.[(triple10)] @1: Anne is nice.[(((triple3) -> rule1))] Anne is quiet.[(((triple2) -> rule2))] Dave is blue.[(((triple6) -> rule3) OR ((((triple8) -> rule1)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
((triple8) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
((triple5) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Anne is nice.
("Anne" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple6) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2