Bob is big. Bob is blue. Bob is cold. Bob is furry. Bob is kind. Bob is round. Bob is young. Dave is big. Dave is furry. Dave is kind. Dave is round. Dave is young. Erin is young. Gary is cold. Gary is kind. Cold things are blue. If something is furry then it is cold. Cold things are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Bob is young.
True
1
proof
[(triple7)]
("Bob" "is" "young" "+")
triple7
Dave is not kind.
False
1
inv-proof
[(triple10)]
("Dave" "is" "kind" "-")
triple10
Gary is big.
True
2
proof
[(((triple14) -> rule3))]
("Gary" "is" "big" "+")
((triple14) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple14) -> rule3))]
("Gary" "is" "big" "-")
((triple14) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Dave is blue.
True
3
proof
[(((((triple9) -> rule2)) -> rule1))]
("Dave" "is" "blue" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule1))]
("Dave" "is" "blue" "-")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not blue.
Unknown
inv-rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Bob is big.[(triple1 OR ((triple3) -> rule3) OR ((((triple4) -> rule2)) -> rule3))] Bob is blue.[(triple2 OR ((triple3) -> rule1) OR ((((triple4) -> rule2)) -> rule1))] Bob is cold.[(triple3 OR ((triple4) -> rule2))] Bob is furry.[(triple4)] Bob is kind.[(triple5)] Bob is round.[(triple6)] Bob is young.[(triple7)] Dave is big.[(triple8 OR ((((triple9) -> rule2)) -> rule3))] Dave is furry.[(triple9)] Dave is kind.[(triple10)] Dave is round.[(triple11)] Dave is young.[(triple12)] Erin is young.[(triple13)] Gary is cold.[(triple14)] Gary is kind.[(triple15)] @1: Dave is cold.[(((triple9) -> rule2))] Gary is big.[(((triple14) -> rule3))] Gary is blue.[(((triple14) -> rule1))] @2: Dave is blue.[(((((triple9) -> rule2)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple3) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
((triple4) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is round.
("Dave" "is" "round" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
Erin is young.
("Erin" "is" "young" "+")
triple13
Gary is cold.
("Gary" "is" "cold" "+")
triple14
Gary is kind.
("Gary" "is" "kind" "+")
triple15
Dave is cold.
("Dave" "is" "cold" "+")
((triple9) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple14) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple14) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2