Anne is green. Charlie is blue. Charlie is green. Charlie is round. Fiona is green. Fiona is nice. Harry is round. If someone is young and kind then they are blue. All quiet people are blue. All kind people are nice. All blue, nice people are kind. Green people are blue. All green, nice people are blue. If someone is nice then they are young. If someone is kind and blue then they are quiet.
Anne is green.
("Anne" "is" "green" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is young and kind then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
All kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All blue, nice people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
All green, nice people are blue.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice then they are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and blue then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
Anne is green.
True
1
proof
[(triple1)]
("Anne" "is" "green" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "green" "-")
triple3
Fiona is blue.
True
2
proof
[(((triple5) -> rule5) OR ((triple5 triple6) -> rule6))]
("Fiona" "is" "blue" "+")
((triple5) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple5 triple6) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "blue" "-")
((triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Harry is not quiet.
Unknown
inv-rconc
[@3: Harry is quiet.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule1 <- FAIL)]]
("Harry" "is" "quiet" "-")
Anne is nice.
Unknown
rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Anne" "is" "nice" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Anne is green.[(triple1)] Charlie is blue.[(triple2 OR ((triple3) -> rule5))] Charlie is green.[(triple3)] Charlie is round.[(triple4)] Fiona is green.[(triple5)] Fiona is nice.[(triple6)] Harry is round.[(triple7)] @1: Anne is blue.[(((triple1) -> rule5))] Fiona is blue.[(((triple5) -> rule5) OR ((triple5 triple6) -> rule6))] Fiona is young.[(((triple6) -> rule7))] @2: Fiona is kind.[(((((triple5) -> rule5) triple6) -> rule4) OR ((((triple5 triple6) -> rule6) triple6) -> rule4))] @3: Fiona is quiet.[(((((((triple5) -> rule5) triple6) -> rule4) ((triple5) -> rule5)) -> rule8) OR ((((((triple5) -> rule5) triple6) -> rule4) ((triple5 triple6) -> rule6)) -> rule8) OR ((((((triple5 triple6) -> rule6) triple6) -> rule4) ((triple5) -> rule5)) -> rule8) OR ((((((triple5 triple6) -> rule6) triple6) -> rule4) ((triple5 triple6) -> rule6)) -> rule8))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
((triple3) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple5
Fiona is nice.
("Fiona" "is" "nice" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple5) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple5 triple6) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple6) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple5) -> (rule5 % int2)) triple6) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple5 triple6) -> (rule6 % int2)) triple6) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((((triple5) -> (rule5 % int3)) triple6) -> (rule4 % int2)) ((triple5) -> (rule5 % int3))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple5) -> (rule5 % int3)) triple6) -> (rule4 % int2)) ((triple5 triple6) -> (rule6 % int3))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple5 triple6) -> (rule6 % int3)) triple6) -> (rule4 % int2)) ((triple5) -> (rule5 % int3))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple5 triple6) -> (rule6 % int3)) triple6) -> (rule4 % int2)) ((triple5 triple6) -> (rule6 % int3))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3