Dave is big. Dave is cold. Dave is not red. Dave is not smart. Dave is white. Erin is big. Erin is blue. Erin is smart. Erin is white. Harry is big. Harry is not blue. Harry is cold. Harry is red. Harry is rough. Harry is smart. Harry is white. If something is red and big then it is rough. If something is cold and big then it is rough. If Harry is not smart then Harry is not big. If something is red then it is white. If Dave is smart then Dave is white. Smart things are cold. If something is smart and not white then it is blue. If Harry is not blue and Harry is not smart then Harry is rough.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not smart.
("Dave" "is" "smart" "-")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is red and big then it is rough.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is cold and big then it is rough.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If Harry is not smart then Harry is not big.
((("Harry" "is" "smart" "~")) -> ("Harry" "is" "big" "-"))
If something is red then it is white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If Dave is smart then Dave is white.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "white" "+"))
Smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If something is smart and not white then it is blue.
((("something" "is" "smart" "+") ("something" "is" "white" "~")) -> ("something" "is" "blue" "+"))
If Harry is not blue and Harry is not smart then Harry is rough.
((("Harry" "is" "blue" "~") ("Harry" "is" "smart" "~")) -> ("Harry" "is" "rough" "+"))
Dave is cold.
True
1
proof
[(triple2)]
("Dave" "is" "cold" "+")
triple2
Erin is not smart.
False
1
inv-proof
[(triple8)]
("Erin" "is" "smart" "-")
triple8
Dave is rough.
True
3
proof
[(((triple2 triple1) -> rule2))]
("Dave" "is" "rough" "+")
((triple2 triple1) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple8) -> rule6))]
("Erin" "is" "cold" "-")
((triple8) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
True
4
proof
[(((((triple8) -> rule6) triple6) -> rule2))]
("Erin" "is" "rough" "+")
((((triple8) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((((triple8) -> rule6) triple6) -> rule2))]
("Erin" "is" "rough" "-")
((((triple8) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "blue" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Dave is big.[(triple1)] Dave is cold.[(triple2)] Dave is not red.[(triple3)] Dave is not smart.[(triple4)] Dave is white.[(triple5)] Erin is big.[(triple6)] Erin is blue.[(triple7)] Erin is smart.[(triple8)] Erin is white.[(triple9)] Harry is big.[(triple10)] Harry is cold.[(triple12 OR ((triple15) -> rule6))] Harry is not blue.[(triple11)] Harry is red.[(triple13)] Harry is rough.[(triple14 OR ((triple12 triple10) -> rule2) OR ((triple13 triple10) -> rule1) OR ((((triple15) -> rule6) triple10) -> rule2))] Harry is smart.[(triple15)] Harry is white.[(triple16 OR ((triple13) -> rule4))] @1: Dave is rough.[(((triple2 triple1) -> rule2))] Erin is cold.[(((triple8) -> rule6))] @2: Erin is rough.[(((((triple8) -> rule6) triple6) -> rule2))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is not red.
("Dave" "is" "red" "-")
triple3
Dave is not smart.
("Dave" "is" "smart" "-")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
Erin is white.
("Erin" "is" "white" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple12
((triple15) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
((triple12 triple10) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple13 triple10) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple15) -> (rule6 % int2)) triple10) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
((triple13) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple2 triple1) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple8) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple8) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2