Charlie is big. Charlie is kind. Charlie is nice. Charlie is rough. Charlie is not round. Charlie is white. Harry is big. Harry is kind. Harry is nice. Harry is rough. Harry is not round. Harry is white. All white, rough people are big. Blue people are not big. If someone is rough then they are white. If someone is kind and not blue then they are rough. If Charlie is not kind then Charlie is not round. If Harry is white then Harry is kind. If someone is big and not rough then they are round. Kind people are not round.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is white.
("Harry" "is" "white" "+")
All white, rough people are big.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Blue people are not big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "-"))
If someone is rough then they are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is kind and not blue then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "rough" "+"))
If Charlie is not kind then Charlie is not round.
((("Charlie" "is" "kind" "~")) -> ("Charlie" "is" "round" "-"))
If Harry is white then Harry is kind.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "kind" "+"))
If someone is big and not rough then they are round.
((("someone" "is" "big" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "round" "+"))
Kind people are not round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "-"))
Charlie is not round.
True
1
proof
[(triple5 OR ((triple2) -> rule8))]
("Charlie" "is" "round" "-")
triple5
((triple2) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is not white.
False
1
inv-proof
[(triple6 OR ((triple4) -> rule3))]
("Charlie" "is" "white" "-")
triple6
((triple4) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Charlie is big.[(triple1 OR ((triple6 triple4) -> rule1) OR ((((triple4) -> rule3) triple4) -> rule1))] Charlie is kind.[(triple2)] Charlie is nice.[(triple3)] Charlie is not round.[(triple5 OR ((triple2) -> rule8))] Charlie is rough.[(triple4)] Charlie is white.[(triple6 OR ((triple4) -> rule3))] Harry is big.[(triple7 OR ((triple12 triple10) -> rule1) OR ((((triple10) -> rule3) triple10) -> rule1))] Harry is kind.[(triple8 OR ((triple12) -> rule6) OR ((((triple10) -> rule3)) -> rule6))] Harry is nice.[(triple9)] Harry is not round.[(triple11 OR ((triple8) -> rule8) OR ((((triple12) -> rule6)) -> rule8) OR ((((((triple10) -> rule3)) -> rule6)) -> rule8))] Harry is rough.[(triple10)] Harry is white.[(triple12 OR ((triple10) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple6 triple4) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple4) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is not round.
("Charlie" "is" "round" "-")
triple5
((triple2) -> (rule8 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple6
((triple4) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple7
((triple12 triple10) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple10) -> (rule3 % int2)) triple10) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple8
((triple12) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is not round.
("Harry" "is" "round" "-")
triple11
((triple8) -> (rule8 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
((((triple12) -> (rule6 % int2))) -> (rule8 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((triple10) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple10) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1