Anne is green. Anne is nice. Anne is quiet. Anne is red. Anne is young. Charlie is nice. Charlie is red. Charlie is young. Harry is round. Harry is young. All green people are blue. All nice people are quiet.
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
All green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
All nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is nice.
True
1
proof
[(triple6)]
("Charlie" "is" "nice" "+")
triple6
Harry is not round.
False
1
inv-proof
[(triple9)]
("Harry" "is" "round" "-")
triple9
Charlie is quiet.
True
2
proof
[(((triple6) -> rule2))]
("Charlie" "is" "quiet" "+")
((triple6) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "blue" "-")
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "blue" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is green.[(triple1)] Anne is nice.[(triple2)] Anne is quiet.[(triple3 OR ((triple2) -> rule2))] Anne is red.[(triple4)] Anne is young.[(triple5)] Charlie is nice.[(triple6)] Charlie is red.[(triple7)] Charlie is young.[(triple8)] Harry is round.[(triple9)] Harry is young.[(triple10)] @1: Anne is blue.[(((triple1) -> rule1))] Charlie is quiet.[(((triple6) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is red.
("Charlie" "is" "red" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple6) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1