Charlie is smart. Dave is green. Smart people are young. If someone is big then they are smart. Smart, nice people are white. Smart people are young. All big people are green. If Dave is rough then Dave is big.
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Smart, nice people are white.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If Dave is rough then Dave is big.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "big" "+"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Charlie is not smart.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "smart" "-")
triple1
Charlie is young.
True
2
proof
[(((triple1) -> rule1) OR ((triple1) -> rule4))]
("Charlie" "is" "young" "+")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule4))]
("Charlie" "is" "young" "-")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "green" "-")
Dave is smart.
Unknown
rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is smart.[(triple1)] Dave is green.[(triple2)] @1: Charlie is young.[(((triple1) -> rule1) OR ((triple1) -> rule4))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1