Charlie is furry. Charlie is green. Charlie is kind. Charlie is smart. Dave is smart. Erin is green. Gary is kind. If Charlie is furry and Charlie is kind then Charlie is not blue. All cold, furry things are kind. If Erin is smart then Erin is furry. If something is green then it is not cold. All smart things are green. All blue, green things are round.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is green.
("Erin" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If Charlie is furry and Charlie is kind then Charlie is not blue.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "blue" "-"))
All cold, furry things are kind.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If Erin is smart then Erin is furry.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "furry" "+"))
If something is green then it is not cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "-"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All blue, green things are round.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Erin is green.
True
1
proof
[(triple6)]
("Erin" "is" "green" "+")
triple6
Dave is not smart.
False
1
inv-proof
[(triple5)]
("Dave" "is" "smart" "-")
triple5
Charlie is not blue.
True
3
proof
[(((triple1 triple3) -> rule1))]
("Charlie" "is" "blue" "-")
((triple1 triple3) -> (rule1 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Dave is not green.
False
2
inv-proof
[(((triple5) -> rule5))]
("Dave" "is" "green" "-")
((triple5) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not cold.
True
3
proof
[(((((triple5) -> rule5)) -> rule4))]
("Dave" "is" "cold" "-")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is cold.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule4))]
("Dave" "is" "cold" "+")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "furry" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "kind" "+")
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Charlie is furry.[(triple1)] Charlie is green.[(triple2 OR ((triple4) -> rule5))] Charlie is kind.[(triple3)] Charlie is smart.[(triple4)] Dave is smart.[(triple5)] Erin is green.[(triple6)] Gary is kind.[(triple7)] @1: Charlie is not blue.[(((triple1 triple3) -> rule1))] Charlie is not cold.[(((triple2) -> rule4) OR ((((triple4) -> rule5)) -> rule4))] Dave is green.[(((triple5) -> rule5))] Erin is not cold.[(((triple6) -> rule4))] @2: Dave is not cold.[(((((triple5) -> rule5)) -> rule4))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple4) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Charlie is not blue.
("Charlie" "is" "blue" "-")
((triple1 triple3) -> (rule1 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
((triple2) -> (rule4 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple5) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
((triple6) -> (rule4 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Dave is not cold.
("Dave" "is" "cold" "-")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2