Anne is round. Bob is not rough. Charlie is furry. Dave is red. All red people are green. If someone is nice then they are not furry. If someone is rough and furry then they are round. Round, red people are smart. All nice, furry people are not smart. All green people are red. All red people are rough. All green, red people are nice.
Anne is round.
("Anne" "is" "round" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
All red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is nice then they are not furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "-"))
If someone is rough and furry then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Round, red people are smart.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
All nice, furry people are not smart.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "-"))
All green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
All green, red people are nice.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Dave is rough.
True
2
proof
[(((triple4) -> rule7))]
("Dave" "is" "rough" "+")
((triple4) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple4) -> rule7))]
("Dave" "is" "rough" "-")
((triple4) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
True
4
proof
[(((((triple4) -> rule1) triple4) -> rule8))]
("Dave" "is" "nice" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((((triple4) -> rule1) triple4) -> rule8))]
("Dave" "is" "nice" "-")
((((triple4) -> (rule1 % int2)) triple4) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not furry.
True
5
proof
[(((((((triple4) -> rule1) triple4) -> rule8)) -> rule2))]
("Dave" "is" "furry" "-")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule8 % int2))) -> (rule2 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is furry.
False
5
inv-proof
[(((((((triple4) -> rule1) triple4) -> rule8)) -> rule2))]
("Dave" "is" "furry" "+")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule8 % int2))) -> (rule2 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "round" "-")
Charlie is green.
Unknown
rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Charlie" "is" "green" "+")
Bob is not nice.
Unknown
inv-rconc
[@3: Bob is nice.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule6 <- FAIL)]]
("Bob" "is" "nice" "-")
Charlie is round.
Unknown
rconc
[@4: Charlie is round.[CWA. Example of deepest failure = (rule3 <- rule7 <- rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "round" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is round.[(triple1)] Bob is not rough.[(triple2)] Charlie is furry.[(triple3)] Dave is red.[(triple4)] @1: Dave is green.[(((triple4) -> rule1))] Dave is rough.[(((triple4) -> rule7))] @2: Dave is nice.[(((((triple4) -> rule1) triple4) -> rule8))] @3: Dave is not furry.[(((((((triple4) -> rule1) triple4) -> rule8)) -> rule2))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is not rough.
("Bob" "is" "rough" "-")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple4) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not furry.
("Dave" "is" "furry" "-")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule8 % int2))) -> (rule2 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3