Bob is not cold. Charlie is cold. Charlie is furry. Charlie is red. Erin is kind. Erin is smart. Erin is white. Fiona is cold. Fiona is furry. Fiona is kind. Fiona is smart. Fiona is not white. Kind, smart people are quiet. All smart, white people are quiet. All cold people are smart. All red people are kind. If Bob is white then Bob is not quiet. If Charlie is smart and Charlie is white then Charlie is quiet.
Bob is not cold.
("Bob" "is" "cold" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is not white.
("Fiona" "is" "white" "-")
Kind, smart people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All smart, white people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If Bob is white then Bob is not quiet.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "quiet" "-"))
If Charlie is smart and Charlie is white then Charlie is quiet.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "quiet" "+"))
Charlie is furry.
True
1
proof
[(triple3)]
("Charlie" "is" "furry" "+")
triple3
Charlie is not furry.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "furry" "-")
triple3
Charlie is smart.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is not quiet.
False
3
inv-proof
[(((triple10 triple11) -> rule1) OR ((triple10 ((triple8) -> rule3)) -> rule1))]
("Fiona" "is" "quiet" "-")
((triple10 triple11) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple10 ((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Charlie is quiet.
True
5
proof
[(((((triple4) -> rule4) ((triple2) -> rule3)) -> rule1))]
("Charlie" "is" "quiet" "+")
((((triple4) -> (rule4 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not quiet.
False
5
inv-proof
[(((((triple4) -> rule4) ((triple2) -> rule3)) -> rule1))]
("Charlie" "is" "quiet" "-")
((((triple4) -> (rule4 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is quiet.
Unknown
rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "kind" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Bob is not cold.[(triple1)] Charlie is cold.[(triple2)] Charlie is furry.[(triple3)] Charlie is red.[(triple4)] Erin is kind.[(triple5)] Erin is smart.[(triple6)] Erin is white.[(triple7)] Fiona is cold.[(triple8)] Fiona is furry.[(triple9)] Fiona is kind.[(triple10)] Fiona is not white.[(triple12)] Fiona is smart.[(triple11 OR ((triple8) -> rule3))] @1: Charlie is kind.[(((triple4) -> rule4))] Charlie is smart.[(((triple2) -> rule3))] Erin is quiet.[(((triple5 triple6) -> rule1) OR ((triple6 triple7) -> rule2))] Fiona is quiet.[(((triple10 triple11) -> rule1) OR ((triple10 ((triple8) -> rule3)) -> rule1))] @2: Charlie is quiet.[(((((triple4) -> rule4) ((triple2) -> rule3)) -> rule1))]
Bob is not cold.
("Bob" "is" "cold" "-")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
Fiona is not white.
("Fiona" "is" "white" "-")
triple12
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
((triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple5 triple6) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple6 triple7) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple10 triple11) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple10 ((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple4) -> (rule4 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3