Bob is round. Bob is white. Dave is white. Fiona is nice. Fiona is smart. Fiona is not white. Harry is not red. If someone is red and kind then they are smart. If someone is kind and not white then they are smart. If Bob is white then Bob is not quiet. If someone is nice and kind then they are not round. Red people are round. Nice people are kind.
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is not white.
("Fiona" "is" "white" "-")
Harry is not red.
("Harry" "is" "red" "-")
If someone is red and kind then they are smart.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is kind and not white then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "smart" "+"))
If Bob is white then Bob is not quiet.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "quiet" "-"))
If someone is nice and kind then they are not round.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "-"))
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Dave is white.
True
1
proof
[(triple3)]
("Dave" "is" "white" "+")
triple3
Fiona is white.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "white" "+")
triple6
Fiona is kind.
True
2
proof
[(((triple4) -> rule6))]
("Fiona" "is" "kind" "+")
((triple4) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Bob is quiet.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "kind" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is round.[(triple1)] Bob is white.[(triple2)] Dave is white.[(triple3)] Fiona is nice.[(triple4)] Fiona is not white.[(triple6)] Fiona is smart.[(triple5 OR ((((triple4) -> rule6) triple6) -> rule2))] Harry is not red.[(triple7)] @1: Bob is not quiet.[(((triple2) -> rule3))] Fiona is kind.[(((triple4) -> rule6))] @2: Fiona is not round.[(((triple4 ((triple4) -> rule6)) -> rule4))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple4
Fiona is not white.
("Fiona" "is" "white" "-")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple5
((((triple4) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is not red.
("Harry" "is" "red" "-")
triple7
Bob is not quiet.
("Bob" "is" "quiet" "-")
((triple2) -> (rule3 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple4) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not round.
("Fiona" "is" "round" "-")
((triple4 ((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2