Anne is big. Charlie is red. Dave is big. If Charlie is big then Charlie is red. Red, round things are not green. Smart things are green. If something is smart then it is green. All green, round things are smart. If something is round then it is smart. If Dave is big then Dave is smart. If Dave is not kind then Dave is white.
Anne is big.
("Anne" "is" "big" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
If Charlie is big then Charlie is red.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "red" "+"))
Red, round things are not green.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "-"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is smart then it is green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All green, round things are smart.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is round then it is smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If Dave is big then Dave is smart.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "smart" "+"))
If Dave is not kind then Dave is white.
((("Dave" "is" "kind" "~")) -> ("Dave" "is" "white" "+"))
Dave is big.
True
1
proof
[(triple3)]
("Dave" "is" "big" "+")
triple3
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Dave is smart.
True
2
proof
[(((triple3) -> rule7))]
("Dave" "is" "smart" "+")
((triple3) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple3) -> rule7))]
("Dave" "is" "smart" "-")
((triple3) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
True
3
proof
[(((((triple3) -> rule7)) -> rule3) OR ((((triple3) -> rule7)) -> rule4))]
("Dave" "is" "green" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule3) OR ((((triple3) -> rule7)) -> rule4))]
("Dave" "is" "green" "-")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Anne is not green.
Unknown
inv-rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "smart" "+")
Charlie is not green.
Unknown
inv-rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "green" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is big.[(triple1)] Charlie is red.[(triple2)] Dave is big.[(triple3)] @1: Dave is smart.[(((triple3) -> rule7))] @2: Dave is green.[(((((triple3) -> rule7)) -> rule3) OR ((((triple3) -> rule7)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2