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