Dave is nice. Dave is quiet. Dave is white. Fiona is blue. Fiona is not red. Fiona is white. Harry is not blue. Harry is furry. Harry is nice. Harry is quiet. Harry is red. Harry is round. If something is nice and not blue then it is quiet. If something is white and not furry then it is round. If Dave is quiet then Dave is red.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is nice and not blue then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "blue" "~")) -> ("something" "is" "quiet" "+"))
If something is white and not furry then it is round.
((("something" "is" "white" "+") ("something" "is" "furry" "~")) -> ("something" "is" "round" "+"))
If Dave is quiet then Dave is red.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "red" "+"))
Harry is nice.
True
1
proof
[(triple9)]
("Harry" "is" "nice" "+")
triple9
Harry is not quiet.
False
1
inv-proof
[(triple10 OR ((triple9 triple7) -> rule1))]
("Harry" "is" "quiet" "-")
triple10
((triple9 triple7) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Dave is red.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "red" "+")
((triple2) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "red" "-")
((triple2) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is nice.[(triple1)] Dave is quiet.[(triple2)] Dave is white.[(triple3)] Fiona is blue.[(triple4)] Fiona is not red.[(triple5)] Fiona is white.[(triple6)] Harry is furry.[(triple8)] Harry is nice.[(triple9)] Harry is not blue.[(triple7)] Harry is quiet.[(triple10 OR ((triple9 triple7) -> rule1))] Harry is red.[(triple11)] Harry is round.[(triple12)] @1: Dave is red.[(((triple2) -> rule3))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
Fiona is not red.
("Fiona" "is" "red" "-")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is not blue.
("Harry" "is" "blue" "-")
triple7
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
((triple9 triple7) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1