Charlie is red. Charlie is round. Charlie is young. Erin is not young. Gary is round. Harry is cold. Harry is kind. If someone is red and not young then they are kind. Young people are kind. Red people are kind. Furry people are cold. If someone is round then they are red. If Erin is young and Erin is green then Erin is round. If Charlie is green then Charlie is red. Kind people are furry. All cold, round people are green.
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is not young.
("Erin" "is" "young" "-")
Gary is round.
("Gary" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If someone is red and not young then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "kind" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If someone is round then they are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If Erin is young and Erin is green then Erin is round.
((("Erin" "is" "young" "+") ("Erin" "is" "green" "+")) -> ("Erin" "is" "round" "+"))
If Charlie is green then Charlie is red.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "red" "+"))
Kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
All cold, round people are green.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Gary is round.
True
1
proof
[(triple5)]
("Gary" "is" "round" "+")
triple5
Harry is not cold.
False
1
inv-proof
[(triple6 OR ((((triple7) -> rule8)) -> rule4))]
("Harry" "is" "cold" "-")
triple6
((((triple7) -> (rule8 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Gary is red.
True
2
proof
[(((triple5) -> rule5))]
("Gary" "is" "red" "+")
((triple5) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple3) -> rule2) OR ((((triple2) -> rule5)) -> rule3))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is furry.
True
3
proof
[(((((triple1) -> rule3)) -> rule8) OR ((((triple3) -> rule2)) -> rule8) OR ((((((triple2) -> rule5)) -> rule3)) -> rule8))]
("Charlie" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is not furry.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8) OR ((((triple3) -> rule2)) -> rule8) OR ((((((triple2) -> rule5)) -> rule3)) -> rule8))]
("Charlie" "is" "furry" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Gary is furry.
True
4
proof
[(((((((triple5) -> rule5)) -> rule3)) -> rule8))]
("Gary" "is" "furry" "+")
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Charlie is not cold.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule8)) -> rule4) OR ((((((triple3) -> rule2)) -> rule8)) -> rule4) OR ((((((((triple2) -> rule5)) -> rule3)) -> rule8)) -> rule4))]
("Charlie" "is" "cold" "-")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((((triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is green.
True
6
proof
[(((((((((triple1) -> rule3)) -> rule8)) -> rule4) triple2) -> rule9) OR ((((((((triple3) -> rule2)) -> rule8)) -> rule4) triple2) -> rule9) OR ((((((((((triple2) -> rule5)) -> rule3)) -> rule8)) -> rule4) triple2) -> rule9))]
("Charlie" "is" "green" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple2) -> (rule9 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((((((triple3) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple2) -> (rule9 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((((((((triple2) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple2) -> (rule9 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
int5
Gary is not cold.
False
5
inv-proof
[(((((((((triple5) -> rule5)) -> rule3)) -> rule8)) -> rule4))]
("Gary" "is" "cold" "-")
((((((((triple5) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is green.
True
7
proof
[(((((((((((triple5) -> rule5)) -> rule3)) -> rule8)) -> rule4) triple5) -> rule9))]
("Gary" "is" "green" "+")
((((((((((triple5) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple5) -> (rule9 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Gary is not green.
False
7
inv-proof
[(((((((((((triple5) -> rule5)) -> rule3)) -> rule8)) -> rule4) triple5) -> rule9))]
("Gary" "is" "green" "-")
((((((((((triple5) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple5) -> (rule9 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Harry" "is" "green" "+")
Erin is not red.
Unknown
inv-rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is kind.
Unknown
rconc
[@3: Erin is kind.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule6 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not furry.
Unknown
inv-rconc
[@4: Erin is furry.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule5 <- rule6 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is cold.
Unknown
rconc
[@5: Erin is cold.[CWA. Example of deepest failure = (rule4 <- rule8 <- rule3 <- rule5 <- rule6 <- FAIL)]]
("Erin" "is" "cold" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Charlie is red.[(triple1 OR ((triple2) -> rule5) OR ((((((((((triple3) -> rule2)) -> rule8)) -> rule4) triple2) -> rule9)) -> rule7))] Charlie is round.[(triple2)] Charlie is young.[(triple3)] Erin is not young.[(triple4)] Gary is round.[(triple5)] Harry is cold.[(triple6 OR ((((triple7) -> rule8)) -> rule4))] Harry is kind.[(triple7)] @1: Charlie is kind.[(((triple1) -> rule3) OR ((triple3) -> rule2) OR ((((triple2) -> rule5)) -> rule3))] Gary is red.[(((triple5) -> rule5))] Harry is furry.[(((triple7) -> rule8))] @2: Charlie is furry.[(((((triple1) -> rule3)) -> rule8) OR ((((triple3) -> rule2)) -> rule8) OR ((((((triple2) -> rule5)) -> rule3)) -> rule8))] Gary is kind.[(((((triple5) -> rule5)) -> rule3))] @3: Charlie is cold.[(((((((triple1) -> rule3)) -> rule8)) -> rule4) OR ((((((triple3) -> rule2)) -> rule8)) -> rule4) OR ((((((((triple2) -> rule5)) -> rule3)) -> rule8)) -> rule4))] Gary is furry.[(((((((triple5) -> rule5)) -> rule3)) -> rule8))] @4: Charlie is green.[(((((((((triple1) -> rule3)) -> rule8)) -> rule4) triple2) -> rule9) OR ((((((((triple3) -> rule2)) -> rule8)) -> rule4) triple2) -> rule9) OR ((((((((((triple2) -> rule5)) -> rule3)) -> rule8)) -> rule4) triple2) -> rule9))] Gary is cold.[(((((((((triple5) -> rule5)) -> rule3)) -> rule8)) -> rule4))] @5: Gary is green.[(((((((((((triple5) -> rule5)) -> rule3)) -> rule8)) -> rule4) triple5) -> rule9))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
((triple2) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((((((((triple3) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule4 % int3)) triple2) -> (rule9 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Erin is not young.
("Erin" "is" "young" "-")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
((((triple7) -> (rule8 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple5) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple7) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((((triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple2) -> (rule9 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((((((triple3) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple2) -> (rule9 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((((((((triple2) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple2) -> (rule9 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
int5
Gary is cold.
("Gary" "is" "cold" "+")
((((((((triple5) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
((((((((((triple5) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple5) -> (rule9 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5