Bob is quiet. Erin is furry. If Bob is furry and Bob is nice then Bob is not blue. Rough people are nice. All smart people are rough. Quiet people are rough. Blue, young people are furry. Nice, young people are smart. All quiet people are smart. Furry people are not quiet.
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is furry.
("Erin" "is" "furry" "+")
If Bob is furry and Bob is nice then Bob is not blue.
((("Bob" "is" "furry" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "blue" "-"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Blue, young people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Nice, young people are smart.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Furry people are not quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "-"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Erin is not furry.
False
1
inv-proof
[(triple2)]
("Erin" "is" "furry" "-")
triple2
Bob is rough.
True
2
proof
[(((triple1) -> rule4) OR ((((triple1) -> rule7)) -> rule3))]
("Bob" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule4) OR ((((triple1) -> rule7)) -> rule3))]
("Bob" "is" "rough" "-")
((triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is nice.
True
3
proof
[(((((triple1) -> rule4)) -> rule2) OR ((((((triple1) -> rule7)) -> rule3)) -> rule2))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2) OR ((((((triple1) -> rule7)) -> rule3)) -> rule2))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is nice.
Unknown
rconc
[@3: Erin is nice.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule6 <- FAIL)]]
("Erin" "is" "nice" "+")
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "furry" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is quiet.[(triple1)] Erin is furry.[(triple2)] @1: Bob is rough.[(((triple1) -> rule4) OR ((((triple1) -> rule7)) -> rule3))] Bob is smart.[(((triple1) -> rule7))] Erin is not quiet.[(((triple2) -> rule8))] @2: Bob is nice.[(((((triple1) -> rule4)) -> rule2) OR ((((((triple1) -> rule7)) -> rule3)) -> rule2))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is not quiet.
("Erin" "is" "quiet" "-")
((triple2) -> (rule8 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3