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