Charlie is furry. Dave is not blue. Erin is cold. Gary is smart. If someone is kind and not big then they are not smart. If someone is white and kind then they are smart. Cold people are smart. If someone is smart and not furry then they are not white. If someone is smart then they are not white. White people are cold. Kind people are blue. If someone is cold and not white then they are not blue.
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is kind and not big then they are not smart.
((("someone" "is" "kind" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "smart" "-"))
If someone is white and kind then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and not furry then they are not white.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "white" "-"))
If someone is smart then they are not white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "-"))
White people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold and not white then they are not blue.
((("someone" "is" "cold" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "blue" "-"))
Dave is not blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Charlie is not furry.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "furry" "-")
triple1
Erin is smart.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple3) -> rule3))]
("Erin" "is" "smart" "-")
((triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not white.
True
3
proof
[(((((triple3) -> rule3)) -> rule5))]
("Erin" "is" "white" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is white.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5))]
("Erin" "is" "white" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not blue.
True
5
proof
[(((triple3 ((((triple3) -> rule3)) -> rule5)) -> rule8))]
("Erin" "is" "blue" "-")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is not white.
("Erin" "is" "white" "-")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is blue.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule3)) -> rule5)) -> rule8))]
("Erin" "is" "blue" "+")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is not white.
("Erin" "is" "white" "-")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "cold" "+")
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "blue" "-")
Charlie is smart.
Unknown
rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "smart" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Charlie is furry.[(triple1)] Dave is not blue.[(triple2)] Erin is cold.[(triple3)] Gary is smart.[(triple4)] @1: Erin is smart.[(((triple3) -> rule3))] Gary is not white.[(((triple4) -> rule5))] @2: Erin is not white.[(((((triple3) -> rule3)) -> rule5))] @3: Erin is not blue.[(((triple3 ((((triple3) -> rule3)) -> rule5)) -> rule8))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Dave is not blue.
("Dave" "is" "blue" "-")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
((triple4) -> (rule5 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Erin is not white.
("Erin" "is" "white" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is not white.
("Erin" "is" "white" "-")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3