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