Dave is blue. Dave is kind. Dave is rough. Dave is round. Dave is young. Erin is blue. Erin is green. Erin is kind. Erin is round. Gary is cold. Gary is young. Harry is blue. Harry is cold. Harry is green. Harry is kind. Harry is young. If Gary is rough and Gary is blue then Gary is young. Green things are kind. If something is kind and green then it is cold. Kind, rough things are young. If something is rough then it is blue. If Dave is kind and Dave is rough then Dave is round. Kind, green things are rough. If something is green and round then it is cold.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
If Gary is rough and Gary is blue then Gary is young.
((("Gary" "is" "rough" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "young" "+"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is kind and green then it is cold.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Kind, rough things are young.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is rough then it is blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If Dave is kind and Dave is rough then Dave is round.
((("Dave" "is" "kind" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "round" "+"))
Kind, green things are rough.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something is green and round then it is cold.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Erin is green.
True
1
proof
[(triple7)]
("Erin" "is" "green" "+")
triple7
Dave is not blue.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule5))]
("Dave" "is" "blue" "-")
triple1
((triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Dave is blue.[(triple1 OR ((triple3) -> rule5))] Dave is kind.[(triple2)] Dave is rough.[(triple3)] Dave is round.[(triple4 OR ((triple2 triple3) -> rule6))] Dave is young.[(triple5 OR ((triple2 triple3) -> rule4))] Erin is blue.[(triple6 OR ((((triple8 triple7) -> rule7)) -> rule5) OR ((((((triple7) -> rule2) triple7) -> rule7)) -> rule5))] Erin is green.[(triple7)] Erin is kind.[(triple8 OR ((triple7) -> rule2))] Erin is round.[(triple9)] Gary is cold.[(triple10)] Gary is young.[(triple11)] Harry is blue.[(triple12 OR ((((triple15 triple14) -> rule7)) -> rule5) OR ((((((triple14) -> rule2) triple14) -> rule7)) -> rule5))] Harry is cold.[(triple13 OR ((triple15 triple14) -> rule3) OR ((((triple14) -> rule2) triple14) -> rule3))] Harry is green.[(triple14)] Harry is kind.[(triple15 OR ((triple14) -> rule2))] Harry is young.[(triple16 OR ((triple15 ((triple15 triple14) -> rule7)) -> rule4) OR ((((triple14) -> rule2) ((triple15 triple14) -> rule7)) -> rule4) OR ((triple15 ((((triple14) -> rule2) triple14) -> rule7)) -> rule4) OR ((((triple14) -> rule2) ((((triple14) -> rule2) triple14) -> rule7)) -> rule4))] @1: Erin is cold.[(((triple7 triple9) -> rule8) OR ((triple8 triple7) -> rule3) OR ((((triple7) -> rule2) triple7) -> rule3))] Erin is rough.[(((triple8 triple7) -> rule7) OR ((((triple7) -> rule2) triple7) -> rule7))] Harry is rough.[(((triple15 triple14) -> rule7) OR ((((triple14) -> rule2) triple14) -> rule7))] @2: Erin is young.[(((triple8 ((triple8 triple7) -> rule7)) -> rule4) OR ((((triple7) -> rule2) ((triple8 triple7) -> rule7)) -> rule4) OR ((triple8 ((((triple7) -> rule2) triple7) -> rule7)) -> rule4) OR ((((triple7) -> rule2) ((((triple7) -> rule2) triple7) -> rule7)) -> rule4))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple3) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
((triple2 triple3) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple5
((triple2 triple3) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple6
((((triple8 triple7) -> (rule7 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((triple7) -> (rule2 % int3)) triple7) -> (rule7 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((triple7) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple9
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Gary is young.
("Gary" "is" "young" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
((((triple15 triple14) -> (rule7 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple14) -> (rule2 % int3)) triple14) -> (rule7 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
triple13
((triple15 triple14) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple14) -> (rule2 % int2)) triple14) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is kind.
("Harry" "is" "kind" "+")
triple15
((triple14) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple15 ((triple15 triple14) -> (rule7 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple14) -> (rule2 % int3)) ((triple15 triple14) -> (rule7 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((triple15 ((((triple14) -> (rule2 % int3)) triple14) -> (rule7 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((triple14) -> (rule2 % int3)) ((((triple14) -> (rule2 % int3)) triple14) -> (rule7 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((triple7 triple9) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple8 triple7) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple7) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple8 triple7) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple7) -> (rule2 % int2)) triple7) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple15 triple14) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple14) -> (rule2 % int2)) triple14) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple8 ((triple8 triple7) -> (rule7 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple7) -> (rule2 % int3)) ((triple8 triple7) -> (rule7 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((triple8 ((((triple7) -> (rule2 % int3)) triple7) -> (rule7 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple7) -> (rule2 % int3)) ((((triple7) -> (rule2 % int3)) triple7) -> (rule7 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3