Bob is big. Bob is cold. Bob is quiet. Bob is young. Charlie is cold. Charlie is kind. Charlie is quiet. Charlie is rough. Dave is big. Dave is cold. Dave is white. Dave is young. Cold, white things are not kind. If something is quiet and not young then it is not cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Cold, white things are not kind.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "-"))
If something is quiet and not young then it is not cold.
((("something" "is" "quiet" "+") ("something" "is" "young" "~")) -> ("something" "is" "cold" "-"))
Bob is young.
True
1
proof
[(triple4)]
("Bob" "is" "young" "+")
triple4
Bob is not young.
False
1
inv-proof
[(triple4)]
("Bob" "is" "young" "-")
triple4
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is quiet.[(triple3)] Bob is young.[(triple4)] Charlie is cold.[(triple5)] Charlie is kind.[(triple6)] Charlie is quiet.[(triple7)] Charlie is rough.[(triple8)] Dave is big.[(triple9)] Dave is cold.[(triple10)] Dave is white.[(triple11)] Dave is young.[(triple12)] @1: Dave is not kind.[(((triple10 triple11) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Dave is big.
("Dave" "is" "big" "+")
triple9
Dave is cold.
("Dave" "is" "cold" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
Dave is not kind.
("Dave" "is" "kind" "-")
((triple10 triple11) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1