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