Anne is big. Anne is blue. Anne is kind. Anne is not young. Bob is blue. Bob is furry. Bob is kind. Bob is smart. Charlie is furry. Charlie is young. All young, furry people are smart. Smart people are rough. If Anne is smart and Anne is not young then Anne is big.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not young.
("Anne" "is" "young" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is young.
("Charlie" "is" "young" "+")
All young, furry people are smart.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If Anne is smart and Anne is not young then Anne is big.
((("Anne" "is" "smart" "+") ("Anne" "is" "young" "~")) -> ("Anne" "is" "big" "+"))
Anne is blue.
True
1
proof
[(triple2)]
("Anne" "is" "blue" "+")
triple2
Anne is not kind.
False
1
inv-proof
[(triple3)]
("Anne" "is" "kind" "-")
triple3
Bob is rough.
True
2
proof
[(((triple8) -> rule2))]
("Bob" "is" "rough" "+")
((triple8) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple8) -> rule2))]
("Bob" "is" "rough" "-")
((triple8) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is rough.
True
4
proof
[(((((triple10 triple9) -> rule1)) -> rule2))]
("Charlie" "is" "rough" "+")
((((triple10 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not rough.
False
4
inv-proof
[(((((triple10 triple9) -> rule1)) -> rule2))]
("Charlie" "is" "rough" "-")
((((triple10 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is rough.
Unknown
rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is kind.[(triple3)] Anne is not young.[(triple4)] Bob is blue.[(triple5)] Bob is furry.[(triple6)] Bob is kind.[(triple7)] Bob is smart.[(triple8)] Charlie is furry.[(triple9)] Charlie is young.[(triple10)] @1: Bob is rough.[(((triple8) -> rule2))] Charlie is smart.[(((triple10 triple9) -> rule1))] @2: Charlie is rough.[(((((triple10 triple9) -> rule1)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is not young.
("Anne" "is" "young" "-")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
triple5
Bob is furry.
("Bob" "is" "furry" "+")
triple6
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
triple8
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Bob is rough.
("Bob" "is" "rough" "+")
((triple8) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple10 triple9) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple10 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2