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