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