Anne is green. Anne is smart. Anne is young. Bob is green. Bob is kind. Bob is round. Gary is blue. Young, green things are round. If something is smart and young then it is green. Big things are green. If something is big then it is kind. If something is kind and blue then it is smart. If Gary is kind then Gary is smart. All young things are smart. All round, kind things are smart.
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Young, green things are round.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is smart and young then it is green.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is kind and blue then it is smart.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If Gary is kind then Gary is smart.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "smart" "+"))
All young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
All round, kind things are smart.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Gary is blue.
True
1
proof
[(triple7)]
("Gary" "is" "blue" "+")
triple7
Anne is not green.
False
1
inv-proof
[(triple1 OR ((triple2 triple3) -> rule2) OR ((((triple3) -> rule7) triple3) -> rule2))]
("Anne" "is" "green" "-")
triple1
((triple2 triple3) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple3) -> (rule7 % int2)) triple3) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Anne is green.[(triple1 OR ((triple2 triple3) -> rule2) OR ((((triple3) -> rule7) triple3) -> rule2))] Anne is smart.[(triple2 OR ((triple3) -> rule7))] Anne is young.[(triple3)] Bob is green.[(triple4)] Bob is kind.[(triple5)] Bob is round.[(triple6)] Gary is blue.[(triple7)] @1: Anne is round.[(((triple3 triple1) -> rule1) OR ((triple3 ((triple2 triple3) -> rule2)) -> rule1) OR ((triple3 ((((triple3) -> rule7) triple3) -> rule2)) -> rule1))] Bob is smart.[(((triple6 triple5) -> rule8))]
Anne is green.
("Anne" "is" "green" "+")
triple1
((triple2 triple3) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple3) -> (rule7 % int2)) triple3) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple2
((triple3) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Anne is round.
("Anne" "is" "round" "+")
((triple3 triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 ((triple2 triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((triple3 ((((triple3) -> (rule7 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((triple6 triple5) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1