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