Bob is big. Bob is not round. Dave is white. Erin is blue. Erin is round. Fiona is big. Fiona is not furry. All white, round people are smart. If Bob is round then Bob is not furry. Blue people are rough. If Bob is furry then Bob is not rough. If someone is smart then they are round. Furry, rough people are not round. Blue, rough people are big. Rough people are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is not round.
("Bob" "is" "round" "-")
Dave is white.
("Dave" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is not furry.
("Fiona" "is" "furry" "-")
All white, round people are smart.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If Bob is round then Bob is not furry.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "furry" "-"))
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Bob is furry then Bob is not rough.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "rough" "-"))
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Furry, rough people are not round.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "-"))
Blue, rough people are big.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Erin is round.
True
1
proof
[(triple5)]
("Erin" "is" "round" "+")
triple5
Erin is not blue.
False
1
inv-proof
[(triple4)]
("Erin" "is" "blue" "-")
triple4
Erin is rough.
True
2
proof
[(((triple4) -> rule3))]
("Erin" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple4) -> rule3))]
("Erin" "is" "rough" "-")
((triple4) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
True
3
proof
[(((((triple4) -> rule3)) -> rule8))]
("Erin" "is" "white" "+")
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule8))]
("Erin" "is" "white" "-")
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is smart.
True
5
proof
[(((((((triple4) -> rule3)) -> rule8) triple5) -> rule1))]
("Erin" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule8 % int2)) triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not smart.
False
5
inv-proof
[(((((((triple4) -> rule3)) -> rule8) triple5) -> rule1))]
("Erin" "is" "smart" "-")
((((((triple4) -> (rule3 % int3))) -> (rule8 % int2)) triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "+")
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is big.[(triple1)] Bob is not round.[(triple2)] Dave is white.[(triple3)] Erin is blue.[(triple4)] Erin is round.[(triple5)] Fiona is big.[(triple6)] Fiona is not furry.[(triple7)] @1: Erin is rough.[(((triple4) -> rule3))] @2: Erin is big.[(((triple4 ((triple4) -> rule3)) -> rule7))] Erin is white.[(((((triple4) -> rule3)) -> rule8))] @3: Erin is smart.[(((((((triple4) -> rule3)) -> rule8) triple5) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not round.
("Bob" "is" "round" "-")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule8 % int2)) triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3