Anne is red. Anne is rough. Charlie is smart. If someone is smart and nice then they are blue. Big, smart people are young. All smart, big people are red. All rough, red people are nice. If Anne is rough and Anne is nice then Anne is big. All nice, rough people are blue. If someone is nice and rough then they are smart. If someone is nice then they are rough.
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If someone is smart and nice then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Big, smart people are young.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All smart, big people are red.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All rough, red people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If Anne is rough and Anne is nice then Anne is big.
((("Anne" "is" "rough" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "big" "+"))
All nice, rough people are blue.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice and rough then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is red.[(triple1)] Anne is rough.[(triple2)] Charlie is smart.[(triple3)] @1: Anne is nice.[(((triple2 triple1) -> rule4))] @2: Anne is big.[(((triple2 ((triple2 triple1) -> rule4)) -> rule5))] Anne is blue.[(((((triple2 triple1) -> rule4) triple2) -> rule6) OR ((((((triple2 triple1) -> rule4) triple2) -> rule7) ((triple2 triple1) -> rule4)) -> rule1))] Anne is smart.[(((((triple2 triple1) -> rule4) triple2) -> rule7))] @3: Anne is young.[(((((triple2 ((triple2 triple1) -> rule4)) -> rule5) ((((triple2 triple1) -> rule4) triple2) -> rule7)) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
((triple2 triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((triple2 ((triple2 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((triple2 triple1) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((((triple2 triple1) -> (rule4 % int3)) triple2) -> (rule7 % int2)) ((triple2 triple1) -> (rule4 % int3))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((((triple2 triple1) -> (rule4 % int2)) triple2) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple2 ((triple2 triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple2 triple1) -> (rule4 % int4)) triple2) -> (rule7 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4