Dave is white. Fiona is blue. Gary is red. Harry is blue. If something is white then it is red. All red things are quiet.
Dave is white.
("Dave" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If something is white then it is red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Gary is red.
True
1
proof
[(triple3)]
("Gary" "is" "red" "+")
triple3
Dave is not white.
False
1
inv-proof
[(triple1)]
("Dave" "is" "white" "-")
triple1
Dave is red.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "red" "+")
((triple1) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "quiet" "-")
((triple3) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Dave" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Dave" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "red" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "+")
Harry is not quiet.
Unknown
inv-rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "quiet" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is white.[(triple1)] Fiona is blue.[(triple2)] Gary is red.[(triple3)] Harry is blue.[(triple4)] @1: Dave is red.[(((triple1) -> rule1))] Gary is quiet.[(((triple3) -> rule2))] @2: Dave is quiet.[(((((triple1) -> rule1)) -> rule2))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2