Charlie is blue. Dave is big. Dave is blue. Dave is not green. Dave is young. Erin is big. Erin is green. All red, young things are green. If Charlie is big then Charlie is blue. All big things are young. If Dave is round then Dave is green. If Charlie is green and Charlie is not red then Charlie is quiet. If something is green and not young then it is blue.
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
All red, young things are green.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If Charlie is big then Charlie is blue.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "blue" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If Dave is round then Dave is green.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "green" "+"))
If Charlie is green and Charlie is not red then Charlie is quiet.
((("Charlie" "is" "green" "+") ("Charlie" "is" "red" "~")) -> ("Charlie" "is" "quiet" "+"))
If something is green and not young then it is blue.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "blue" "+"))
Dave is not green.
True
1
proof
[(triple4)]
("Dave" "is" "green" "-")
triple4
Dave is green.
False
1
inv-proof
[(triple4)]
("Dave" "is" "green" "+")
triple4
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "young" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Charlie is blue.[(triple1)] Dave is big.[(triple2)] Dave is blue.[(triple3)] Dave is not green.[(triple4)] Dave is young.[(triple5 OR ((triple2) -> rule3))] Erin is big.[(triple6)] Erin is green.[(triple7)] @1: Erin is young.[(((triple6) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is not green.
("Dave" "is" "green" "-")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple5
((triple2) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
Erin is young.
("Erin" "is" "young" "+")
((triple6) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1