Bob is kind. Bob is nice. Bob is quiet. Bob is rough. Bob is round. Dave is not red. Dave is rough. Dave is round. Erin is nice. Erin is rough. If someone is red and not round then they are not nice. If someone is red then they are quiet. If Dave is nice then Dave is quiet. Smart, rough people are red. All rough, nice people are smart. Smart people are rough.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
If someone is red and not round then they are not nice.
((("someone" "is" "red" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "nice" "-"))
If someone is red then they are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is nice then Dave is quiet.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "quiet" "+"))
Smart, rough people are red.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
All rough, nice people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Dave is rough.
True
1
proof
[(triple7)]
("Dave" "is" "rough" "+")
triple7
Dave is not rough.
False
1
inv-proof
[(triple7)]
("Dave" "is" "rough" "-")
triple7
Bob is smart.
True
3
proof
[(((triple4 triple2) -> rule5))]
("Bob" "is" "smart" "+")
((triple4 triple2) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
3
inv-proof
[(((triple4 triple2) -> rule5))]
("Bob" "is" "smart" "-")
((triple4 triple2) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
True
5
proof
[(((((triple4 triple2) -> rule5) triple4) -> rule4))]
("Bob" "is" "red" "+")
((((triple4 triple2) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Erin is not red.
False
5
inv-proof
[(((((triple10 triple9) -> rule5) triple10) -> rule4))]
("Erin" "is" "red" "-")
((((triple10 triple9) -> (rule5 % int2)) triple10) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "smart" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is kind.[(triple1)] Bob is nice.[(triple2)] Bob is quiet.[(triple3 OR ((((((triple4 triple2) -> rule5) triple4) -> rule4)) -> rule2))] Bob is rough.[(triple4)] Bob is round.[(triple5)] Dave is not red.[(triple6)] Dave is rough.[(triple7)] Dave is round.[(triple8)] Erin is nice.[(triple9)] Erin is rough.[(triple10)] @1: Bob is smart.[(((triple4 triple2) -> rule5))] Erin is smart.[(((triple10 triple9) -> rule5))] @2: Bob is red.[(((((triple4 triple2) -> rule5) triple4) -> rule4))] Erin is red.[(((((triple10 triple9) -> rule5) triple10) -> rule4))] @3: Erin is quiet.[(((((((triple10 triple9) -> rule5) triple10) -> rule4)) -> rule2))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((((((triple4 triple2) -> (rule5 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Dave is not red.
("Dave" "is" "red" "-")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Dave is round.
("Dave" "is" "round" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Bob is smart.
("Bob" "is" "smart" "+")
((triple4 triple2) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple10 triple9) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple4 triple2) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple10 triple9) -> (rule5 % int2)) triple10) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple10 triple9) -> (rule5 % int3)) triple10) -> (rule4 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3