Dave is green. Dave is not white. Erin is smart. Erin is white. Fiona is blue. Fiona is green. Fiona is red. Fiona is white. Harry is green. Harry is red. Harry is smart. Harry is white. If Erin is red and Erin is not smart then Erin is nice. If someone is smart then they are nice. All green, red people are blue. Red, smart people are blue. If Dave is rough and Dave is nice then Dave is blue. If someone is white and blue then they are not rough.
Dave is green.
("Dave" "is" "green" "+")
Dave is not white.
("Dave" "is" "white" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If Erin is red and Erin is not smart then Erin is nice.
((("Erin" "is" "red" "+") ("Erin" "is" "smart" "~")) -> ("Erin" "is" "nice" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All green, red people are blue.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Red, smart people are blue.
((("someone" "is" "red" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If Dave is rough and Dave is nice then Dave is blue.
((("Dave" "is" "rough" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "blue" "+"))
If someone is white and blue then they are not rough.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "-"))
Fiona is red.
True
1
proof
[(triple7)]
("Fiona" "is" "red" "+")
triple7
Fiona is not green.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "green" "-")
triple6
Erin is nice.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Harry is not blue.
False
3
inv-proof
[(((triple10 triple11) -> rule4) OR ((triple9 triple10) -> rule3))]
("Harry" "is" "blue" "-")
((triple10 triple11) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple9 triple10) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not rough.
True
5
proof
[(((triple12 ((triple10 triple11) -> rule4)) -> rule6) OR ((triple12 ((triple9 triple10) -> rule3)) -> rule6))]
("Harry" "is" "rough" "-")
((triple12 ((triple10 triple11) -> (rule4 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple12 ((triple9 triple10) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is rough.
False
5
inv-proof
[(((triple12 ((triple10 triple11) -> rule4)) -> rule6) OR ((triple12 ((triple9 triple10) -> rule3)) -> rule6))]
("Harry" "is" "rough" "+")
((triple12 ((triple10 triple11) -> (rule4 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple12 ((triple9 triple10) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "nice" "+")
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "blue" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Dave is green.[(triple1)] Dave is not white.[(triple2)] Erin is smart.[(triple3)] Erin is white.[(triple4)] Fiona is blue.[(triple5 OR ((triple6 triple7) -> rule3))] Fiona is green.[(triple6)] Fiona is red.[(triple7)] Fiona is white.[(triple8)] Harry is green.[(triple9)] Harry is red.[(triple10)] Harry is smart.[(triple11)] Harry is white.[(triple12)] @1: Erin is nice.[(((triple3) -> rule2))] Fiona is not rough.[(((triple8 triple5) -> rule6) OR ((triple8 ((triple6 triple7) -> rule3)) -> rule6))] Harry is blue.[(((triple10 triple11) -> rule4) OR ((triple9 triple10) -> rule3))] Harry is nice.[(((triple11) -> rule2))] @2: Harry is not rough.[(((triple12 ((triple10 triple11) -> rule4)) -> rule6) OR ((triple12 ((triple9 triple10) -> rule3)) -> rule6))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is not white.
("Dave" "is" "white" "-")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
((triple6 triple7) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Fiona is white.
("Fiona" "is" "white" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Fiona is not rough.
("Fiona" "is" "rough" "-")
((triple8 triple5) -> (rule6 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
((triple8 ((triple6 triple7) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((triple10 triple11) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple9 triple10) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple11) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
((triple12 ((triple10 triple11) -> (rule4 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple12 ((triple9 triple10) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2