Bob is kind. Bob is nice. Bob is round. Bob is white. Bob is young. Charlie is nice. Charlie is round. Charlie is smart. Charlie is white. Charlie is young. If someone is kind then they are white. Nice people are white. All round, nice people are young.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
All round, nice people are young.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Charlie is nice.
True
1
proof
[(triple6)]
("Charlie" "is" "nice" "+")
triple6
Bob is not young.
False
1
inv-proof
[(triple5 OR ((triple3 triple2) -> rule3))]
("Bob" "is" "young" "-")
triple5
((triple3 triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is kind.[(triple1)] Bob is nice.[(triple2)] Bob is round.[(triple3)] Bob is white.[(triple4 OR ((triple1) -> rule1) OR ((triple2) -> rule2))] Bob is young.[(triple5 OR ((triple3 triple2) -> rule3))] Charlie is nice.[(triple6)] Charlie is round.[(triple7)] Charlie is smart.[(triple8)] Charlie is white.[(triple9 OR ((triple6) -> rule2))] Charlie is young.[(triple10 OR ((triple7 triple6) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple2) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple5
((triple3 triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Charlie is white.
("Charlie" "is" "white" "+")
triple9
((triple6) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple10
((triple7 triple6) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1