Erin is blue. Erin is cold. Erin is kind. Erin is red. Gary is cold. Gary is furry. Gary is kind. Gary is red. Harry is cold. Harry is quiet. Harry is red. Harry is young. Furry, quiet people are kind. If Erin is furry and Erin is cold then Erin is young. If someone is quiet then they are furry. If Gary is kind then Gary is furry. Cold people are red. If Gary is furry and Gary is blue then Gary is young. All furry, kind people are quiet. If someone is kind and red then they are blue.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
Furry, quiet people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Erin is furry and Erin is cold then Erin is young.
((("Erin" "is" "furry" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "young" "+"))
If someone is quiet then they are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If Gary is kind then Gary is furry.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "furry" "+"))
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If Gary is furry and Gary is blue then Gary is young.
((("Gary" "is" "furry" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "young" "+"))
All furry, kind people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind and red then they are blue.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Erin is blue.
True
1
proof
[(triple1 OR ((triple3 triple4) -> rule8) OR ((triple3 ((triple2) -> rule5)) -> rule8))]
("Erin" "is" "blue" "+")
triple1
((triple3 triple4) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple3 ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Harry is not cold.
False
1
inv-proof
[(triple9)]
("Harry" "is" "cold" "-")
triple9
Harry is furry.
True
2
proof
[(((triple10) -> rule3))]
("Harry" "is" "furry" "+")
((triple10) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Gary is not blue.
False
3
inv-proof
[(((triple7 triple8) -> rule8) OR ((triple7 ((triple5) -> rule5)) -> rule8))]
("Gary" "is" "blue" "-")
((triple7 triple8) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple7 ((triple5) -> (rule5 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Harry is kind.
True
4
proof
[(((((triple10) -> rule3) triple10) -> rule1))]
("Harry" "is" "kind" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not kind.
False
4
inv-proof
[(((((triple10) -> rule3) triple10) -> rule1))]
("Harry" "is" "kind" "-")
((((triple10) -> (rule3 % int2)) triple10) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
True
6
proof
[(((((((triple10) -> rule3) triple10) -> rule1) triple11) -> rule8) OR ((((((triple10) -> rule3) triple10) -> rule1) ((triple9) -> rule5)) -> rule8))]
("Harry" "is" "blue" "+")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule1 % int2)) triple11) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple10) -> (rule3 % int4)) triple10) -> (rule1 % int3)) ((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is not blue.
False
6
inv-proof
[(((((((triple10) -> rule3) triple10) -> rule1) triple11) -> rule8) OR ((((((triple10) -> rule3) triple10) -> rule1) ((triple9) -> rule5)) -> rule8))]
("Harry" "is" "blue" "-")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule1 % int2)) triple11) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple10) -> (rule3 % int4)) triple10) -> (rule1 % int3)) ((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Erin is not quiet.
Unknown
inv-rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is furry.
Unknown
rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Erin" "is" "furry" "+")
@0: Erin is blue.[(triple1 OR ((triple3 triple4) -> rule8) OR ((triple3 ((triple2) -> rule5)) -> rule8))] Erin is cold.[(triple2)] Erin is kind.[(triple3)] Erin is red.[(triple4 OR ((triple2) -> rule5))] Gary is cold.[(triple5)] Gary is furry.[(triple6 OR ((triple7) -> rule4))] Gary is kind.[(triple7)] Gary is red.[(triple8 OR ((triple5) -> rule5))] Harry is cold.[(triple9)] Harry is quiet.[(triple10)] Harry is red.[(triple11 OR ((triple9) -> rule5))] Harry is young.[(triple12)] @1: Gary is blue.[(((triple7 triple8) -> rule8) OR ((triple7 ((triple5) -> rule5)) -> rule8))] Gary is quiet.[(((triple6 triple7) -> rule7) OR ((((triple7) -> rule4) triple7) -> rule7))] Harry is furry.[(((triple10) -> rule3))] @2: Gary is young.[(((triple6 ((triple7 triple8) -> rule8)) -> rule6) OR ((((triple7) -> rule4) ((triple7 triple8) -> rule8)) -> rule6) OR ((triple6 ((triple7 ((triple5) -> rule5)) -> rule8)) -> rule6) OR ((((triple7) -> rule4) ((triple7 ((triple5) -> rule5)) -> rule8)) -> rule6))] Harry is kind.[(((((triple10) -> rule3) triple10) -> rule1))] @3: Harry is blue.[(((((((triple10) -> rule3) triple10) -> rule1) triple11) -> rule8) OR ((((((triple10) -> rule3) triple10) -> rule1) ((triple9) -> rule5)) -> rule8))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple3 triple4) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple3 ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
((triple2) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
((triple7) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple8
((triple5) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
((triple9) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple12
Gary is blue.
("Gary" "is" "blue" "+")
((triple7 triple8) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple7 ((triple5) -> (rule5 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple6 triple7) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple7) -> (rule4 % int2)) triple7) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple10) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple6 ((triple7 triple8) -> (rule8 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple7) -> (rule4 % int3)) ((triple7 triple8) -> (rule8 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((triple6 ((triple7 ((triple5) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((triple7) -> (rule4 % int4)) ((triple7 ((triple5) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule1 % int2)) triple11) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple10) -> (rule3 % int4)) triple10) -> (rule1 % int3)) ((triple9) -> (rule5 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4