Bob is blue. Dave is white. Fiona is rough. Blue things are white. If something is smart and rough then it is white. Round things are smart. White things are red. If Bob is white and Bob is smart then Bob is red. All blue, red things are not round.
Bob is blue.
("Bob" "is" "blue" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If something is smart and rough then it is white.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
White things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If Bob is white and Bob is smart then Bob is red.
((("Bob" "is" "white" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "red" "+"))
All blue, red things are not round.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "-"))
Fiona is rough.
True
1
proof
[(triple3)]
("Fiona" "is" "rough" "+")
triple3
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is white.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "red" "-")
((triple2) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Bob is red.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Bob" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not red.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Bob" "is" "red" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "smart" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "smart" "+")
Fiona is not red.
Unknown
inv-rconc
[@3: Fiona is red.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
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" "+")
@0: Bob is blue.[(triple1)] Dave is white.[(triple2)] Fiona is rough.[(triple3)] @1: Bob is white.[(((triple1) -> rule1))] Dave is red.[(((triple2) -> rule4))] @2: Bob is red.[(((((triple1) -> rule1)) -> rule4))] @3: Bob is not round.[(((triple1 ((((triple1) -> rule1)) -> rule4)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not round.
("Bob" "is" "round" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3