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