Bob is blue. Dave is red. Fiona is green. If Bob is white and Bob is quiet then Bob is red. White people are red. If someone is red then they are green. If someone is round then they are green. If someone is blue then they are white. If someone is round then they are white. Quiet people are nice. If Dave is round then Dave is green.
Bob is blue.
("Bob" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is green.
("Fiona" "is" "green" "+")
If Bob is white and Bob is quiet then Bob is red.
((("Bob" "is" "white" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "red" "+"))
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is blue then they are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If Dave is round then Dave is green.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "green" "+"))
Fiona is green.
True
1
proof
[(triple3)]
("Fiona" "is" "green" "+")
triple3
Fiona is not green.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "green" "-")
triple3
Dave is green.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "green" "+")
((triple2) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "green" "-")
((triple2) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Bob is red.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("Bob" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not red.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("Bob" "is" "red" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
True
4
proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule3))]
("Bob" "is" "green" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not green.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule3))]
("Bob" "is" "green" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "nice" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "white" "-")
Fiona is red.
Unknown
rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "red" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is blue.[(triple1)] Dave is red.[(triple2)] Fiona is green.[(triple3)] @1: Bob is white.[(((triple1) -> rule5))] Dave is green.[(((triple2) -> rule3))] @2: Bob is red.[(((((triple1) -> rule5)) -> rule2))] @3: Bob is green.[(((((((triple1) -> rule5)) -> rule2)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3