Charlie is smart. Dave is nice. Erin is big. If someone is nice then they are smart. If Charlie is not nice then Charlie is furry.
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
If someone is nice then they are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is not nice then Charlie is furry.
((("Charlie" "is" "nice" "~")) -> ("Charlie" "is" "furry" "+"))
Dave is nice.
True
1
proof
[(triple2)]
("Dave" "is" "nice" "+")
triple2
Erin is not big.
False
1
inv-proof
[(triple3)]
("Erin" "is" "big" "-")
triple3
Dave is smart.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "furry" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Charlie is smart.[(triple1)] Dave is nice.[(triple2)] Erin is big.[(triple3)] @1: Dave is smart.[(((triple2) -> rule1))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1