Anne is red. Bob is rough. Charlie is kind. Dave is young. If Anne is young then Anne is kind. If someone is rough and kind then they are green. Rough people are kind. If someone is red then they are big. If someone is young then they are big. If someone is kind and green then they are red. All green people are kind. Young, green people are rough.
Anne is red.
("Anne" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
If Anne is young then Anne is kind.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "kind" "+"))
If someone is rough and kind then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is young then they are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and green then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Young, green people are rough.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Charlie is kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Charlie is not kind.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "kind" "-")
triple3
Anne is not green.
Unknown
inv-rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("Anne" "is" "green" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is red.[(triple1)] Bob is rough.[(triple2)] Charlie is kind.[(triple3)] Dave is young.[(triple4)] @1: Anne is big.[(((triple1) -> rule4))] Bob is kind.[(((triple2) -> rule3))] Dave is big.[(((triple4) -> rule5))] @2: Bob is green.[(((triple2 ((triple2) -> rule3)) -> rule2))] @3: Bob is red.[(((((triple2) -> rule3) ((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6))] @4: Bob is big.[(((((((triple2) -> rule3) ((triple2 ((triple2) -> rule3)) -> rule2)) -> rule6)) -> rule4))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple4) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple2) -> (rule3 % int3)) ((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((((((triple2) -> (rule3 % int4)) ((triple2 ((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4