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