Anne is blue. Anne is smart. Anne is young. Bob is kind. Dave is white. Dave is young. Gary is blue. All blue things are young. All kind things are blue. Smart things are blue. White, young things are not kind. Young things are smart. If Bob is cold and Bob is big then Bob is white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
White, young things are not kind.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "-"))
Young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If Bob is cold and Bob is big then Bob is white.
((("Bob" "is" "cold" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "white" "+"))
Bob is kind.
True
1
proof
[(triple4)]
("Bob" "is" "kind" "+")
triple4
Anne is not smart.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule5) OR ((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "smart" "-")
triple2
((triple3) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Gary is young.
True
2
proof
[(((triple7) -> rule1))]
("Gary" "is" "young" "+")
((triple7) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple7) -> rule1))]
("Gary" "is" "young" "-")
((triple7) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
True
3
proof
[(((((triple7) -> rule1)) -> rule5))]
("Gary" "is" "smart" "+")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule3))]
("Dave" "is" "blue" "-")
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Bob is smart.
True
4
proof
[(((((((triple4) -> rule2)) -> rule1)) -> rule5))]
("Bob" "is" "smart" "+")
((((((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not smart.
False
4
inv-proof
[(((((((triple4) -> rule2)) -> rule1)) -> rule5))]
("Bob" "is" "smart" "-")
((((((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "white" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Anne is blue.[(triple1 OR ((triple2) -> rule3) OR ((((triple3) -> rule5)) -> rule3))] Anne is smart.[(triple2 OR ((triple3) -> rule5) OR ((((triple1) -> rule1)) -> rule5))] Anne is young.[(triple3 OR ((triple1) -> rule1) OR ((((triple2) -> rule3)) -> rule1))] Bob is kind.[(triple4)] Dave is white.[(triple5)] Dave is young.[(triple6)] Gary is blue.[(triple7)] @1: Bob is blue.[(((triple4) -> rule2))] Dave is not kind.[(((triple5 triple6) -> rule4))] Dave is smart.[(((triple6) -> rule5))] Gary is young.[(((triple7) -> rule1))] @2: Bob is young.[(((((triple4) -> rule2)) -> rule1))] Dave is blue.[(((((triple6) -> rule5)) -> rule3))] Gary is smart.[(((((triple7) -> rule1)) -> rule5))] @3: Bob is smart.[(((((((triple4) -> rule2)) -> rule1)) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple2) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple2
((triple3) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple3
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple4) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Dave is not kind.
("Dave" "is" "kind" "-")
((triple5 triple6) -> (rule4 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple6) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple7) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3