Bob is not furry. Charlie is blue. All green people are blue. Blue people are smart. All smart people are big. If someone is red and not smart then they are furry. Furry, big people are not red. If someone is green and not big then they are white. All big people are white. If Charlie is white and Charlie is smart then Charlie is furry.
Bob is not furry.
("Bob" "is" "furry" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
All green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If someone is red and not smart then they are furry.
((("someone" "is" "red" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "furry" "+"))
Furry, big people are not red.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "-"))
If someone is green and not big then they are white.
((("someone" "is" "green" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "white" "+"))
All big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If Charlie is white and Charlie is smart then Charlie is furry.
((("Charlie" "is" "white" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "furry" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Bob is furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Charlie is smart.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "smart" "-")
((triple2) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Charlie" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Charlie" "is" "big" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is white.
True
4
proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule7))]
("Charlie" "is" "white" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not white.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule7))]
("Charlie" "is" "white" "-")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Bob is not white.
Unknown
inv-rconc
[@4: Bob is white.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule2 <- rule1 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not big.
Unknown
inv-rconc
[@3: Bob is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is not furry.[(triple1)] Charlie is blue.[(triple2)] @1: Charlie is smart.[(((triple2) -> rule2))] @2: Charlie is big.[(((((triple2) -> rule2)) -> rule3))] @3: Charlie is white.[(((((((triple2) -> rule2)) -> rule3)) -> rule7))] @4: Charlie is furry.[(((((((((triple2) -> rule2)) -> rule3)) -> rule7) ((triple2) -> rule2)) -> rule8))] @5: Charlie is not red.[(((((((((((triple2) -> rule2)) -> rule3)) -> rule7) ((triple2) -> rule2)) -> rule8) ((((triple2) -> rule2)) -> rule3)) -> rule5))]
Bob is not furry.
("Bob" "is" "furry" "-")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((((triple2) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((triple2) -> (rule2 % int4))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is not red.
("Charlie" "is" "red" "-")
((((((((((triple2) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) ((triple2) -> (rule2 % int5))) -> (rule8 % int2)) ((((triple2) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule5 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
int5