Anne is smart. Bob is red. Dave is smart. Fiona is green. If something is round then it is red. Red things are smart. If Anne is young and Anne is red then Anne is furry. All smart things are round. Red things are furry. All red things are round.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Anne is young and Anne is red then Anne is furry.
((("Anne" "is" "young" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "furry" "+"))
All smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
All red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Bob is smart.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "round" "-")
((triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("Anne" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Dave is not red.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule1))]
("Dave" "is" "red" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
True
4
proof
[(((((((triple3) -> rule4)) -> rule1)) -> rule5))]
("Dave" "is" "furry" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Anne is not furry.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule1)) -> rule5))]
("Anne" "is" "furry" "-")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@3: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule4 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is red.
Unknown
rconc
[@3: Fiona is red.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule2 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not round.
Unknown
inv-rconc
[@4: Fiona is round.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule1 <- rule6 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is furry.
Unknown
rconc
[@4: Fiona is furry.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule4 <- rule2 <- FAIL)]]
("Fiona" "is" "furry" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is smart.[(triple1)] Bob is red.[(triple2)] Dave is smart.[(triple3)] Fiona is green.[(triple4)] @1: Anne is round.[(((triple1) -> rule4))] Bob is furry.[(((triple2) -> rule5))] Bob is round.[(((triple2) -> rule6) OR ((((triple2) -> rule2)) -> rule4))] Bob is smart.[(((triple2) -> rule2))] Dave is round.[(((triple3) -> rule4))] @2: Anne is red.[(((((triple1) -> rule4)) -> rule1))] Dave is red.[(((((triple3) -> rule4)) -> rule1))] @3: Anne is furry.[(((((((triple1) -> rule4)) -> rule1)) -> rule5))] Dave is furry.[(((((((triple3) -> rule4)) -> rule1)) -> rule5))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple3) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3