Charlie is young. Dave is not blue. Harry is red. If someone is blue then they are green. If someone is young then they are red. If Charlie is red then Charlie is green. All cold, young people are furry. If someone is young then they are cold. If someone is smart and not green then they are not cold. All smart, red people are cold. If someone is cold then they are smart.
Charlie is young.
("Charlie" "is" "young" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Harry is red.
("Harry" "is" "red" "+")
If someone is blue then they are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If Charlie is red then Charlie is green.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "green" "+"))
All cold, young people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If someone is young then they are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart and not green then they are not cold.
((("someone" "is" "smart" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "cold" "-"))
All smart, red people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Harry is red.
True
1
proof
[(triple3)]
("Harry" "is" "red" "+")
triple3
Harry is not red.
False
1
inv-proof
[(triple3)]
("Harry" "is" "red" "-")
triple3
Charlie is red.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "red" "+")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "red" "-")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not smart.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule8))]
("Charlie" "is" "smart" "-")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "furry" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not cold.
Unknown
inv-rconc
[@3: Harry is cold.[CWA. Example of deepest failure = (rule7 <- rule8 <- rule5 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Charlie is young.[(triple1)] Dave is not blue.[(triple2)] Harry is red.[(triple3)] @1: Charlie is cold.[(((triple1) -> rule5))] Charlie is red.[(((triple1) -> rule2))] @2: Charlie is furry.[(((((triple1) -> rule5) triple1) -> rule4))] Charlie is green.[(((((triple1) -> rule2)) -> rule3))] Charlie is smart.[(((((triple1) -> rule5)) -> rule8))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Dave is not blue.
("Dave" "is" "blue" "-")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2