Anne is big. Anne is cold. Anne is red. Anne is young. Bob is big. Bob is blue. Bob is cold. Bob is red. Bob is young. Dave is cold. Dave is white. Gary is big. Gary is cold. Gary is red. Gary is smart. Gary is white. All smart things are blue. Big things are smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
All smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Bob is not red.
False
1
inv-proof
[(triple8)]
("Bob" "is" "red" "-")
triple8
Anne is smart.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple5) -> rule2))]
("Bob" "is" "smart" "-")
((triple5) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is blue.
Unknown
rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "blue" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is red.[(triple3)] Anne is young.[(triple4)] Bob is big.[(triple5)] Bob is blue.[(triple6 OR ((((triple5) -> rule2)) -> rule1))] Bob is cold.[(triple7)] Bob is red.[(triple8)] Bob is young.[(triple9)] Dave is cold.[(triple10)] Dave is white.[(triple11)] Gary is big.[(triple12)] Gary is cold.[(triple13)] Gary is red.[(triple14)] Gary is smart.[(triple15 OR ((triple12) -> rule2))] Gary is white.[(triple16)] @1: Anne is smart.[(((triple1) -> rule2))] Bob is smart.[(((triple5) -> rule2))] Gary is blue.[(((triple15) -> rule1) OR ((((triple12) -> rule2)) -> rule1))] @2: Anne is blue.[(((((triple1) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is blue.
("Bob" "is" "blue" "+")
triple6
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
triple8
Bob is young.
("Bob" "is" "young" "+")
triple9
Dave is cold.
("Dave" "is" "cold" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is cold.
("Gary" "is" "cold" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
((triple12) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple16
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple5) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple15) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple12) -> (rule2 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2