Charlie is cold. Erin is blue. Gary is furry. Harry is young. All blue people are big. All cold, furry people are young. Young, blue people are kind. Big people are young. If someone is green and kind then they are furry. Green people are cold.
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is young.
("Harry" "is" "young" "+")
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
All cold, furry people are young.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Young, blue people are kind.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is green and kind then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Erin is blue.
True
1
proof
[(triple2)]
("Erin" "is" "blue" "+")
triple2
Gary is not furry.
False
1
inv-proof
[(triple3)]
("Gary" "is" "furry" "-")
triple3
Erin is big.
True
2
proof
[(((triple2) -> rule1))]
("Erin" "is" "big" "+")
((triple2) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple2) -> rule1))]
("Erin" "is" "big" "-")
((triple2) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("Erin" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not young.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("Erin" "is" "young" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is kind.
True
5
proof
[(((((((triple2) -> rule1)) -> rule4) triple2) -> rule3))]
("Erin" "is" "kind" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not kind.
False
5
inv-proof
[(((((((triple2) -> rule1)) -> rule4) triple2) -> rule3))]
("Erin" "is" "kind" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is furry.
Unknown
rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "furry" "+")
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "kind" "-")
Erin is furry.
Unknown
rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "furry" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Charlie is cold.[(triple1)] Erin is blue.[(triple2)] Gary is furry.[(triple3)] Harry is young.[(triple4)] @1: Erin is big.[(((triple2) -> rule1))] @2: Erin is young.[(((((triple2) -> rule1)) -> rule4))] @3: Erin is kind.[(((((((triple2) -> rule1)) -> rule4) triple2) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
((triple2) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3