Charlie is green. Charlie is red. Charlie is smart. Charlie is white. Charlie is young. Fiona is cold. Fiona is green. Fiona is rough. Fiona is white. Harry is cold. Harry is green. Harry is red. Harry is rough. Harry is smart. Harry is white. Harry is young. If something is young and smart then it is rough. Cold things are white. If Harry is rough and Harry is cold then Harry is smart. If something is young and cold then it is rough. If something is white and smart then it is rough. All white, young things are rough. Red things are white. If Charlie is rough and Charlie is white then Charlie is cold.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is young and smart then it is rough.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If Harry is rough and Harry is cold then Harry is smart.
((("Harry" "is" "rough" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "smart" "+"))
If something is young and cold then it is rough.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is white and smart then it is rough.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
All white, young things are rough.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If Charlie is rough and Charlie is white then Charlie is cold.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "cold" "+"))
Harry is young.
True
1
proof
[(triple16)]
("Harry" "is" "young" "+")
triple16
Charlie is not white.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule7))]
("Charlie" "is" "white" "-")
triple4
((triple2) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Charlie is green.[(triple1)] Charlie is red.[(triple2)] Charlie is smart.[(triple3)] Charlie is white.[(triple4 OR ((triple2) -> rule7))] Charlie is young.[(triple5)] Fiona is cold.[(triple6)] Fiona is green.[(triple7)] Fiona is rough.[(triple8)] Fiona is white.[(triple9 OR ((triple6) -> rule2))] Harry is cold.[(triple10)] Harry is green.[(triple11)] Harry is red.[(triple12)] Harry is rough.[(triple13 OR ((triple15 triple14) -> rule5) OR ((triple15 triple16) -> rule6) OR ((triple16 triple10) -> rule4) OR ((triple16 triple14) -> rule1) OR ((((triple10) -> rule2) triple14) -> rule5) OR ((((triple10) -> rule2) triple16) -> rule6) OR ((((triple12) -> rule7) triple14) -> rule5) OR ((((triple12) -> rule7) triple16) -> rule6))] Harry is smart.[(triple14 OR ((triple13 triple10) -> rule3) OR ((((triple15 triple16) -> rule6) triple10) -> rule3) OR ((((triple16 triple10) -> rule4) triple10) -> rule3) OR ((((((triple10) -> rule2) triple16) -> rule6) triple10) -> rule3) OR ((((((triple12) -> rule7) triple16) -> rule6) triple10) -> rule3))] Harry is white.[(triple15 OR ((triple10) -> rule2) OR ((triple12) -> rule7))] Harry is young.[(triple16)] @1: Charlie is rough.[(((triple4 triple3) -> rule5) OR ((triple4 triple5) -> rule6) OR ((triple5 triple3) -> rule1) OR ((((triple2) -> rule7) triple3) -> rule5) OR ((((triple2) -> rule7) triple5) -> rule6))] @2: Charlie is cold.[(((((triple4 triple3) -> rule5) triple4) -> rule8) OR ((((triple4 triple5) -> rule6) triple4) -> rule8) OR ((((triple5 triple3) -> rule1) triple4) -> rule8) OR ((((triple4 triple3) -> rule5) ((triple2) -> rule7)) -> rule8) OR ((((triple4 triple5) -> rule6) ((triple2) -> rule7)) -> rule8) OR ((((triple5 triple3) -> rule1) ((triple2) -> rule7)) -> rule8) OR ((((((triple2) -> rule7) triple3) -> rule5) triple4) -> rule8) OR ((((((triple2) -> rule7) triple5) -> rule6) triple4) -> rule8) OR ((((((triple2) -> rule7) triple3) -> rule5) ((triple2) -> rule7)) -> rule8) OR ((((((triple2) -> rule7) triple5) -> rule6) ((triple2) -> rule7)) -> rule8))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
((triple2) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Fiona is white.
("Fiona" "is" "white" "+")
triple9
((triple6) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
((triple15 triple14) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple15 triple16) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple16 triple10) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple16 triple14) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple10) -> (rule2 % int2)) triple14) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple10) -> (rule2 % int2)) triple16) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple12) -> (rule7 % int2)) triple14) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple12) -> (rule7 % int2)) triple16) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple14
((triple13 triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple15 triple16) -> (rule6 % int2)) triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple16 triple10) -> (rule4 % int2)) triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple10) -> (rule2 % int3)) triple16) -> (rule6 % int2)) triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple12) -> (rule7 % int3)) triple16) -> (rule6 % int2)) triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple10) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple12) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple16
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4 triple3) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple4 triple5) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple5 triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple2) -> (rule7 % int2)) triple3) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple2) -> (rule7 % int2)) triple5) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple4 triple3) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple4 triple5) -> (rule6 % int2)) triple4) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple5 triple3) -> (rule1 % int2)) triple4) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple4 triple3) -> (rule5 % int3)) ((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((triple4 triple5) -> (rule6 % int3)) ((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((triple5 triple3) -> (rule1 % int3)) ((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple2) -> (rule7 % int3)) triple3) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple2) -> (rule7 % int3)) triple5) -> (rule6 % int2)) triple4) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple2) -> (rule7 % int3)) triple3) -> (rule5 % int2)) ((triple2) -> (rule7 % int3))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple2) -> (rule7 % int3)) triple5) -> (rule6 % int2)) ((triple2) -> (rule7 % int3))) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3