Charlie is big. Dave is white. Erin is young. Harry is white. All smart people are nice. If someone is white then they are big. If someone is big then they are nice.
Charlie is big.
("Charlie" "is" "big" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is white.
("Harry" "is" "white" "+")
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is white then they are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Dave is white.
True
1
proof
[(triple2)]
("Dave" "is" "white" "+")
triple2
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Harry is big.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "big" "+")
((triple4) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is nice.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Dave" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule3))]
("Harry" "is" "nice" "-")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Erin is not nice.
Unknown
inv-rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "big" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Charlie is big.[(triple1)] Dave is white.[(triple2)] Erin is young.[(triple3)] Harry is white.[(triple4)] @1: Charlie is nice.[(((triple1) -> rule3))] Dave is big.[(((triple2) -> rule2))] Harry is big.[(((triple4) -> rule2))] @2: Dave is nice.[(((((triple2) -> rule2)) -> rule3))] Harry is nice.[(((((triple4) -> rule2)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2