Bob is cold. Bob is nice. Bob is rough. Charlie is not cold. Charlie is green. Charlie is not kind. Charlie is not nice. Charlie is round. Dave is green. Dave is kind. Dave is nice. Dave is rough. Rough people are nice. If Dave is not rough then Dave is nice. If someone is rough and not nice then they are green. If someone is nice then they are green. All kind people are quiet. Cold people are quiet. Quiet, nice people are cold. If Charlie is nice and Charlie is not green then Charlie is kind.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If Dave is not rough then Dave is nice.
((("Dave" "is" "rough" "~")) -> ("Dave" "is" "nice" "+"))
If someone is rough and not nice then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "green" "+"))
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Quiet, nice people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is nice and Charlie is not green then Charlie is kind.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "green" "~")) -> ("Charlie" "is" "kind" "+"))
Bob is nice.
True
1
proof
[(triple2 OR ((triple3) -> rule1))]
("Bob" "is" "nice" "+")
triple2
((triple3) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Charlie is not green.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "green" "-")
triple5
Bob is quiet.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Bob is cold.[(triple1)] Bob is nice.[(triple2 OR ((triple3) -> rule1))] Bob is rough.[(triple3)] Charlie is green.[(triple5)] Charlie is not cold.[(triple4)] Charlie is not kind.[(triple6)] Charlie is not nice.[(triple7)] Charlie is round.[(triple8)] Dave is green.[(triple9 OR ((triple11) -> rule4) OR ((((triple12) -> rule1)) -> rule4))] Dave is kind.[(triple10)] Dave is nice.[(triple11 OR ((triple12) -> rule1))] Dave is rough.[(triple12)] @1: Bob is green.[(((triple2) -> rule4) OR ((((triple3) -> rule1)) -> rule4))] Bob is quiet.[(((triple1) -> rule6))] Dave is quiet.[(((triple10) -> rule5))] @2: Dave is cold.[(((((triple10) -> rule5) triple11) -> rule7) OR ((((triple10) -> rule5) ((triple12) -> rule1)) -> rule7))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((triple3) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple4
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple6
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
((triple11) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
triple11
((triple12) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple12
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple10) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple10) -> (rule5 % int2)) triple11) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple10) -> (rule5 % int3)) ((triple12) -> (rule1 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3