Bob is big. Bob is cold. Bob is furry. Bob is green. Bob is round. Bob is smart. Bob is white. Dave is green. Dave is round. Erin is cold. If someone is round then they are white. White people are furry. Furry people are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
White people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Erin is cold.
True
1
proof
[(triple10)]
("Erin" "is" "cold" "+")
triple10
Erin is not cold.
False
1
inv-proof
[(triple10)]
("Erin" "is" "cold" "-")
triple10
Dave is white.
True
2
proof
[(((triple9) -> rule1))]
("Dave" "is" "white" "+")
((triple9) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple9) -> rule1))]
("Dave" "is" "white" "-")
((triple9) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
True
3
proof
[(((((triple9) -> rule1)) -> rule2))]
("Dave" "is" "furry" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule2))]
("Dave" "is" "furry" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
True
4
proof
[(((((((triple9) -> rule1)) -> rule2)) -> rule3))]
("Dave" "is" "big" "+")
((((((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not big.
False
4
inv-proof
[(((((((triple9) -> rule1)) -> rule2)) -> rule3))]
("Dave" "is" "big" "-")
((((((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Erin is not big.
Unknown
inv-rconc
[@3: Erin is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not furry.
Unknown
inv-rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is big.[(triple1 OR ((triple3) -> rule3) OR ((((triple7) -> rule2)) -> rule3) OR ((((((triple5) -> rule1)) -> rule2)) -> rule3))] Bob is cold.[(triple2)] Bob is furry.[(triple3 OR ((triple7) -> rule2) OR ((((triple5) -> rule1)) -> rule2))] Bob is green.[(triple4)] Bob is round.[(triple5)] Bob is smart.[(triple6)] Bob is white.[(triple7 OR ((triple5) -> rule1))] Dave is green.[(triple8)] Dave is round.[(triple9)] Erin is cold.[(triple10)] @1: Dave is white.[(((triple9) -> rule1))] @2: Dave is furry.[(((((triple9) -> rule1)) -> rule2))] @3: Dave is big.[(((((((triple9) -> rule1)) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple7) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple5) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
Erin is cold.
("Erin" "is" "cold" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
((triple9) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3