Dave is nice. Dave is red. Dave is rough. Dave is smart. Dave is white. Fiona is blue. Fiona is red. If Fiona is quiet and Fiona is red then Fiona is white. Quiet things are rough. If something is red then it is white. If Dave is rough and Dave is quiet then Dave is white. If Dave is smart then Dave is white. All white things are blue.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If Fiona is quiet and Fiona is red then Fiona is white.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "red" "+")) -> ("Fiona" "is" "white" "+"))
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is red then it is white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If Dave is rough and Dave is quiet then Dave is white.
((("Dave" "is" "rough" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "white" "+"))
If Dave is smart then Dave is white.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "white" "+"))
All white things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Dave is rough.
True
1
proof
[(triple3)]
("Dave" "is" "rough" "+")
triple3
Dave is not white.
False
1
inv-proof
[(triple5 OR ((triple2) -> rule3) OR ((triple4) -> rule5))]
("Dave" "is" "white" "-")
triple5
((triple2) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple4) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Dave is nice.[(triple1)] Dave is red.[(triple2)] Dave is rough.[(triple3)] Dave is smart.[(triple4)] Dave is white.[(triple5 OR ((triple2) -> rule3) OR ((triple4) -> rule5))] Fiona is blue.[(triple6 OR ((((triple7) -> rule3)) -> rule6))] Fiona is red.[(triple7)] @1: Dave is blue.[(((triple5) -> rule6) OR ((((triple2) -> rule3)) -> rule6) OR ((((triple4) -> rule5)) -> rule6))] Fiona is white.[(((triple7) -> rule3))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
((triple2) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple4) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
((triple5) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((triple7) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1