Bob is big. Bob is kind. Bob is nice. Bob is rough. Charlie is big. Charlie is not furry. Charlie is nice. Charlie is rough. Charlie is round. Gary is round. Gary is smart. Harry is round. All round people are rough. Rough people are smart. If Harry is rough and Harry is smart then Harry is kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is round.
("Harry" "is" "round" "+")
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If Harry is rough and Harry is smart then Harry is kind.
((("Harry" "is" "rough" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "kind" "+"))
Charlie is big.
True
1
proof
[(triple5)]
("Charlie" "is" "big" "+")
triple5
Bob is not nice.
False
1
inv-proof
[(triple3)]
("Bob" "is" "nice" "-")
triple3
Harry is rough.
True
2
proof
[(((triple12) -> rule1))]
("Harry" "is" "rough" "+")
((triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple8) -> rule2) OR ((((triple9) -> rule1)) -> rule2))]
("Charlie" "is" "smart" "-")
((triple8) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Harry is smart.
True
3
proof
[(((((triple12) -> rule1)) -> rule2))]
("Harry" "is" "smart" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule2))]
("Harry" "is" "smart" "-")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
True
6
proof
[(((((triple12) -> rule1) ((((triple12) -> rule1)) -> rule2)) -> rule3))]
("Harry" "is" "kind" "+")
((((triple12) -> (rule1 % int3)) ((((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not kind.
False
6
inv-proof
[(((((triple12) -> rule1) ((((triple12) -> rule1)) -> rule2)) -> rule3))]
("Harry" "is" "kind" "-")
((((triple12) -> (rule1 % int3)) ((((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Bob is big.[(triple1)] Bob is kind.[(triple2)] Bob is nice.[(triple3)] Bob is rough.[(triple4)] Charlie is big.[(triple5)] Charlie is nice.[(triple7)] Charlie is not furry.[(triple6)] Charlie is rough.[(triple8 OR ((triple9) -> rule1))] Charlie is round.[(triple9)] Gary is round.[(triple10)] Gary is smart.[(triple11 OR ((((triple10) -> rule1)) -> rule2))] Harry is round.[(triple12)] @1: Bob is smart.[(((triple4) -> rule2))] Charlie is smart.[(((triple8) -> rule2) OR ((((triple9) -> rule1)) -> rule2))] Gary is rough.[(((triple10) -> rule1))] Harry is rough.[(((triple12) -> rule1))] @2: Harry is smart.[(((((triple12) -> rule1)) -> rule2))] @3: Harry is kind.[(((((triple12) -> rule1) ((((triple12) -> rule1)) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
((triple9) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple11
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple12
Bob is smart.
("Bob" "is" "smart" "+")
((triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple8) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple12) -> (rule1 % int3)) ((((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3