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