Dave is blue. Erin is furry. Gary is young. Harry is green. Green things are not cold. If something is young then it is green. If Dave is green and Dave is not cold then Dave is blue.
Dave is blue.
("Dave" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Green things are not cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "-"))
If something is young then it is green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If Dave is green and Dave is not cold then Dave is blue.
((("Dave" "is" "green" "+") ("Dave" "is" "cold" "~")) -> ("Dave" "is" "blue" "+"))
Gary is young.
True
1
proof
[(triple3)]
("Gary" "is" "young" "+")
triple3
Dave is not blue.
False
1
inv-proof
[(triple1)]
("Dave" "is" "blue" "-")
triple1
Gary is green.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "green" "+")
((triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "green" "-")
((triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not cold.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("Gary" "is" "cold" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Gary" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "green" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Dave is blue.[(triple1)] Erin is furry.[(triple2)] Gary is young.[(triple3)] Harry is green.[(triple4)] @1: Gary is green.[(((triple3) -> rule2))] Harry is not cold.[(((triple4) -> rule1))] @2: Gary is not cold.[(((((triple3) -> rule2)) -> rule1))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
((triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((triple4) -> (rule1 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Gary is not cold.
("Gary" "is" "cold" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2