Bob is red. Fiona is blue. Fiona is kind. All red things are furry. Quiet, cold things are red. Cold things are furry. If something is furry then it is kind. All kind things are round. If Bob is blue and Bob is red then Bob is round.
Bob is red.
("Bob" "is" "red" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
All red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Quiet, cold things are red.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
All kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If Bob is blue and Bob is red then Bob is round.
((("Bob" "is" "blue" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "round" "+"))
Fiona is kind.
True
1
proof
[(triple3)]
("Fiona" "is" "kind" "+")
triple3
Fiona is not blue.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "blue" "-")
triple2
Bob is furry.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Fiona is not round.
False
2
inv-proof
[(((triple3) -> rule5))]
("Fiona" "is" "round" "-")
((triple3) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Bob is kind.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Bob" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Bob" "is" "kind" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
("Bob" "is" "round" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not round.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
("Bob" "is" "round" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Fiona is not furry.
Unknown
inv-rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Bob is red.[(triple1)] Fiona is blue.[(triple2)] Fiona is kind.[(triple3)] @1: Bob is furry.[(((triple1) -> rule1))] Fiona is round.[(((triple3) -> rule5))] @2: Bob is kind.[(((((triple1) -> rule1)) -> rule4))] @3: Bob is round.[(((((((triple1) -> rule1)) -> rule4)) -> rule5))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3