Bob is smart. Fiona is furry. If Bob is not smart then Bob is not quiet. If Bob is furry then Bob is quiet. All cold things are blue. If something is quiet then it is blue. If something is smart then it is furry. If Bob is green and Bob is not quiet then Bob is not red.
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
If Bob is not smart then Bob is not quiet.
((("Bob" "is" "smart" "~")) -> ("Bob" "is" "quiet" "-"))
If Bob is furry then Bob is quiet.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "quiet" "+"))
All cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If Bob is green and Bob is not quiet then Bob is not red.
((("Bob" "is" "green" "+") ("Bob" "is" "quiet" "~")) -> ("Bob" "is" "red" "-"))
Fiona is furry.
True
1
proof
[(triple2)]
("Fiona" "is" "furry" "+")
triple2
Fiona is not furry.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "furry" "-")
triple2
Bob is furry.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "furry" "-")
((triple1) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
True
4
proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule4))]
("Bob" "is" "blue" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not blue.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule4))]
("Bob" "is" "blue" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
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" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Bob is smart.[(triple1)] Fiona is furry.[(triple2)] @1: Bob is furry.[(((triple1) -> rule5))] @2: Bob is quiet.[(((((triple1) -> rule5)) -> rule2))] @3: Bob is blue.[(((((((triple1) -> rule5)) -> rule2)) -> rule4))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3