Charlie is furry. Dave is nice. Fiona is green. Harry is not green. If someone is nice then they are not red. If Charlie is white then Charlie is quiet. All furry people are big. All furry, white people are quiet. If Dave is nice then Dave is not quiet. All nice people are furry. If someone is white then they are green. If someone is red then they are white.
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is not green.
("Harry" "is" "green" "-")
If someone is nice then they are not red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "-"))
If Charlie is white then Charlie is quiet.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "quiet" "+"))
All furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All furry, white people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is nice then Dave is not quiet.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "quiet" "-"))
All nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is red then they are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Dave is nice.
True
1
proof
[(triple2)]
("Dave" "is" "nice" "+")
triple2
Dave is not nice.
False
1
inv-proof
[(triple2)]
("Dave" "is" "nice" "-")
triple2
Charlie is big.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "big" "+")
((triple1) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is quiet.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is big.
True
3
proof
[(((((triple2) -> rule6)) -> rule3))]
("Dave" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("Dave" "is" "big" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "white" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "white" "+")
Harry is not big.
Unknown
inv-rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Charlie is furry.[(triple1)] Dave is nice.[(triple2)] Fiona is green.[(triple3)] Harry is not green.[(triple4)] @1: Charlie is big.[(((triple1) -> rule3))] Dave is furry.[(((triple2) -> rule6))] Dave is not quiet.[(((triple2) -> rule5))] Dave is not red.[(((triple2) -> rule1))] @2: Dave is big.[(((((triple2) -> rule6)) -> rule3))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Harry is not green.
("Harry" "is" "green" "-")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple2) -> (rule5 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is not red.
("Dave" "is" "red" "-")
((triple2) -> (rule1 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2