Anne is blue. Anne is furry. Anne is red. Anne is rough. Bob is red. Bob is smart. Bob is young. Gary is blue. Gary is furry. Gary is quiet. If someone is quiet then they are rough. All furry, smart people are red. All rough people are smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
All furry, smart people are red.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Gary is not blue.
False
1
inv-proof
[(triple8)]
("Gary" "is" "blue" "-")
triple8
Gary is rough.
True
2
proof
[(((triple10) -> rule1))]
("Gary" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple4) -> rule3))]
("Anne" "is" "smart" "-")
((triple4) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is smart.
True
3
proof
[(((((triple10) -> rule1)) -> rule3))]
("Gary" "is" "smart" "+")
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple10) -> rule1)) -> rule3))]
("Gary" "is" "smart" "-")
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is red.
True
5
proof
[(((triple9 ((((triple10) -> rule1)) -> rule3)) -> rule2))]
("Gary" "is" "red" "+")
((triple9 ((((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not red.
False
5
inv-proof
[(((triple9 ((((triple10) -> rule1)) -> rule3)) -> rule2))]
("Gary" "is" "red" "-")
((triple9 ((((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "rough" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is red.[(triple3 OR ((triple2 ((triple4) -> rule3)) -> rule2))] Anne is rough.[(triple4)] Bob is red.[(triple5)] Bob is smart.[(triple6)] Bob is young.[(triple7)] Gary is blue.[(triple8)] Gary is furry.[(triple9)] Gary is quiet.[(triple10)] @1: Anne is smart.[(((triple4) -> rule3))] Gary is rough.[(((triple10) -> rule1))] @2: Gary is smart.[(((((triple10) -> rule1)) -> rule3))] @3: Gary is red.[(((triple9 ((((triple10) -> rule1)) -> rule3)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple2 ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Anne is smart.
("Anne" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple9 ((((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3