Anne is round. Anne is young. Bob is big. Bob is furry. Bob is smart. Bob is white. Charlie is big. Big people are green. If Charlie is young then Charlie is green. If Charlie is green then Charlie is furry. If someone is round and green then they are furry. If someone is furry and green then they are white. If Charlie is big and Charlie is green then Charlie is smart.
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If Charlie is young then Charlie is green.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "green" "+"))
If Charlie is green then Charlie is furry.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "furry" "+"))
If someone is round and green then they are furry.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and green then they are white.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Charlie is big and Charlie is green then Charlie is smart.
((("Charlie" "is" "big" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "smart" "+"))
Charlie is big.
True
1
proof
[(triple7)]
("Charlie" "is" "big" "+")
triple7
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Bob is green.
True
2
proof
[(((triple3) -> rule1))]
("Bob" "is" "green" "+")
((triple3) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple3) -> rule1))]
("Bob" "is" "green" "-")
((triple3) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Anne is not furry.
Unknown
inv-rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "green" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Anne is round.[(triple1)] Anne is young.[(triple2)] Bob is big.[(triple3)] Bob is furry.[(triple4)] Bob is smart.[(triple5)] Bob is white.[(triple6 OR ((triple4 ((triple3) -> rule1)) -> rule5))] Charlie is big.[(triple7)] @1: Bob is green.[(((triple3) -> rule1))] Charlie is green.[(((triple7) -> rule1))] @2: Charlie is furry.[(((((triple7) -> rule1)) -> rule3))] Charlie is smart.[(((triple7 ((triple7) -> rule1)) -> rule6))] @3: Charlie is white.[(((((((triple7) -> rule1)) -> rule3) ((triple7) -> rule1)) -> rule5))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple4 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple3) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple7) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2)) ((triple7) -> (rule1 % int3))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3