Anne is blue. Charlie is young. Dave is round. Erin is blue. If something is round then it is green. All round, green things are nice.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is blue.
("Erin" "is" "blue" "+")
If something is round then it is green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All round, green things are nice.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Dave is not round.
False
1
inv-proof
[(triple3)]
("Dave" "is" "round" "-")
triple3
Dave is green.
True
2
proof
[(((triple3) -> rule1))]
("Dave" "is" "green" "+")
((triple3) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "green" "-")
((triple3) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule2))]
("Dave" "is" "nice" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule2))]
("Dave" "is" "nice" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "green" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Anne is blue.[(triple1)] Charlie is young.[(triple2)] Dave is round.[(triple3)] Erin is blue.[(triple4)] @1: Dave is green.[(((triple3) -> rule1))] @2: Dave is nice.[(((triple3 ((triple3) -> rule1)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2