Charlie is big. Erin is kind. Gary is blue. Gary is cold. Gary is white. Harry is big. Harry is blue. Harry is cold. Harry is furry. Harry is kind. Harry is red. Harry is not white. If something is red then it is cold. If something is white and not kind then it is cold. Big, white things are cold. If something is blue then it is big. If something is blue and big then it is furry. If something is big and furry then it is red.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not white.
("Harry" "is" "white" "-")
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is white and not kind then it is cold.
((("something" "is" "white" "+") ("something" "is" "kind" "~")) -> ("something" "is" "cold" "+"))
Big, white things are cold.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is blue and big then it is furry.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is big and furry then it is red.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Harry is blue.
True
1
proof
[(triple7)]
("Harry" "is" "blue" "+")
triple7
Harry is not big.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule4))]
("Harry" "is" "big" "-")
triple6
((triple7) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Gary is big.
True
2
proof
[(((triple3) -> rule4))]
("Gary" "is" "big" "+")
((triple3) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple3) -> rule4))]
("Gary" "is" "big" "-")
((triple3) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule5))]
("Gary" "is" "furry" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not furry.
False
4
inv-proof
[(((triple3 ((triple3) -> rule4)) -> rule5))]
("Gary" "is" "furry" "-")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
True
7
proof
[(((((triple3) -> rule4) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6))]
("Gary" "is" "red" "+")
((((triple3) -> (rule4 % int3)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not red.
False
7
inv-proof
[(((((triple3) -> rule4) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6))]
("Gary" "is" "red" "-")
((((triple3) -> (rule4 % int3)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Erin is not red.
Unknown
inv-rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Erin" "is" "red" "-")
Charlie is red.
Unknown
rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Charlie" "is" "red" "+")
Erin is not cold.
Unknown
inv-rconc
[@3: Erin is cold.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule4 <- FAIL)]]
("Erin" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@3: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule5 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is big.[(triple1)] Erin is kind.[(triple2)] Gary is blue.[(triple3)] Gary is cold.[(triple4 OR ((((triple3) -> rule4) triple5) -> rule3) OR ((((((triple3) -> rule4) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6)) -> rule1))] Gary is white.[(triple5)] Harry is big.[(triple6 OR ((triple7) -> rule4))] Harry is blue.[(triple7)] Harry is cold.[(triple8 OR ((triple11) -> rule1) OR ((((triple6 triple9) -> rule6)) -> rule1) OR ((((triple6 ((triple7 triple6) -> rule5)) -> rule6)) -> rule1) OR ((((((triple7) -> rule4) triple9) -> rule6)) -> rule1) OR ((((((triple7) -> rule4) ((triple7 triple6) -> rule5)) -> rule6)) -> rule1) OR ((((triple6 ((triple7 ((triple7) -> rule4)) -> rule5)) -> rule6)) -> rule1) OR ((((((triple7) -> rule4) ((triple7 ((triple7) -> rule4)) -> rule5)) -> rule6)) -> rule1))] Harry is furry.[(triple9 OR ((triple7 triple6) -> rule5) OR ((triple7 ((triple7) -> rule4)) -> rule5))] Harry is kind.[(triple10)] Harry is not white.[(triple12)] Harry is red.[(triple11 OR ((triple6 triple9) -> rule6) OR ((triple6 ((triple7 triple6) -> rule5)) -> rule6) OR ((((triple7) -> rule4) triple9) -> rule6) OR ((((triple7) -> rule4) ((triple7 triple6) -> rule5)) -> rule6) OR ((triple6 ((triple7 ((triple7) -> rule4)) -> rule5)) -> rule6) OR ((((triple7) -> rule4) ((triple7 ((triple7) -> rule4)) -> rule5)) -> rule6))] @1: Gary is big.[(((triple3) -> rule4))] @2: Gary is furry.[(((triple3 ((triple3) -> rule4)) -> rule5))] @3: Gary is red.[(((((triple3) -> rule4) ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule6))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
((((triple3) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple3) -> (rule4 % int4)) ((triple3 ((triple3) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
((triple7) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
((triple11) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple6 triple9) -> (rule6 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple6 ((triple7 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple7) -> (rule4 % int3)) triple9) -> (rule6 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple7) -> (rule4 % int4)) ((triple7 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple6 ((triple7 ((triple7) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((((triple7) -> (rule4 % int4)) ((triple7 ((triple7) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple7 triple6) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple7 ((triple7) -> (rule4 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is not white.
("Harry" "is" "white" "-")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple11
((triple6 triple9) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple6 ((triple7 triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple7) -> (rule4 % int2)) triple9) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple7) -> (rule4 % int3)) ((triple7 triple6) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((triple6 ((triple7 ((triple7) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple7) -> (rule4 % int3)) ((triple7 ((triple7) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((triple3) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple3) -> (rule4 % int3)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3