Bob is nice. Bob is rough. Bob is round. Charlie is cold. Charlie is green. Charlie is nice. Charlie is rough. Gary is cold. Gary is furry. Gary is round. All rough things are round. If something is nice then it is cold. All cold things are kind.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
All rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Bob is not round.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule1))]
("Bob" "is" "round" "-")
triple3
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is kind.
True
2
proof
[(((triple4) -> rule3) OR ((((triple6) -> rule2)) -> rule3))]
("Charlie" "is" "kind" "+")
((triple4) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Gary is not kind.
False
2
inv-proof
[(((triple8) -> rule3))]
("Gary" "is" "kind" "-")
((triple8) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Bob is kind.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is nice.[(triple1)] Bob is rough.[(triple2)] Bob is round.[(triple3 OR ((triple2) -> rule1))] Charlie is cold.[(triple4 OR ((triple6) -> rule2))] Charlie is green.[(triple5)] Charlie is nice.[(triple6)] Charlie is rough.[(triple7)] Gary is cold.[(triple8)] Gary is furry.[(triple9)] Gary is round.[(triple10)] @1: Bob is cold.[(((triple1) -> rule2))] Charlie is kind.[(((triple4) -> rule3) OR ((((triple6) -> rule2)) -> rule3))] Charlie is round.[(((triple7) -> rule1))] Gary is kind.[(((triple8) -> rule3))] @2: Bob is kind.[(((((triple1) -> rule2)) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
((triple6) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple8) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2