Dave is blue. Fiona is blue. Gary is round. Harry is nice. If Dave is nice then Dave is rough. If Gary is red and Gary is rough then Gary is smart. If Harry is cold and Harry is smart then Harry is round. If someone is nice then they are round. Nice people are smart. Cold people are blue. If someone is red then they are rough. All round people are rough.
Dave is blue.
("Dave" "is" "blue" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If Dave is nice then Dave is rough.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "rough" "+"))
If Gary is red and Gary is rough then Gary is smart.
((("Gary" "is" "red" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "smart" "+"))
If Harry is cold and Harry is smart then Harry is round.
((("Harry" "is" "cold" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "round" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
Cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Fiona is blue.
True
1
proof
[(triple2)]
("Fiona" "is" "blue" "+")
triple2
Harry is not nice.
False
1
inv-proof
[(triple4)]
("Harry" "is" "nice" "-")
triple4
Gary is rough.
True
2
proof
[(((triple3) -> rule8))]
("Gary" "is" "rough" "+")
((triple3) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple4) -> rule5))]
("Harry" "is" "smart" "-")
((triple4) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "round" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is blue.[(triple1)] Fiona is blue.[(triple2)] Gary is round.[(triple3)] Harry is nice.[(triple4)] @1: Gary is rough.[(((triple3) -> rule8))] Harry is round.[(((triple4) -> rule4))] Harry is smart.[(((triple4) -> rule5))] @2: Harry is rough.[(((((triple4) -> rule4)) -> rule8))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
((triple3) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple4) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple4) -> (rule4 % int2))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2