Anne is smart. Bob is round. Fiona is smart. All smart, round people are white. If someone is kind then they are red. All cold people are kind. If someone is big and smart then they are not kind. If someone is smart then they are cold. If someone is smart then they are round. All cold, smart people are not big. If Bob is not big and Bob is not round then Bob is white.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is round.
("Bob" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
All smart, round people are white.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If someone is kind then they are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is big and smart then they are not kind.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "-"))
If someone is smart then they are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
All cold, smart people are not big.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "-"))
If Bob is not big and Bob is not round then Bob is white.
((("Bob" "is" "big" "~") ("Bob" "is" "round" "~")) -> ("Bob" "is" "white" "+"))
Fiona is smart.
True
1
proof
[(triple3)]
("Fiona" "is" "smart" "+")
triple3
Bob is not round.
False
1
inv-proof
[(triple2)]
("Bob" "is" "round" "-")
triple2
Anne is round.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "round" "+")
((triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "round" "-")
((triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Fiona is kind.
True
3
proof
[(((((triple3) -> rule5)) -> rule3))]
("Fiona" "is" "kind" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not white.
False
4
inv-proof
[(((triple3 ((triple3) -> rule6)) -> rule1))]
("Fiona" "is" "white" "-")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is red.
True
4
proof
[(((((((triple3) -> rule5)) -> rule3)) -> rule2))]
("Fiona" "is" "red" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is not red.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule3)) -> rule2))]
("Fiona" "is" "red" "-")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is kind.
Unknown
rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Bob" "is" "kind" "+")
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is red.
Unknown
rconc
[@3: Bob is red.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule5 <- FAIL)]]
("Bob" "is" "red" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is smart.[(triple1)] Bob is round.[(triple2)] Fiona is smart.[(triple3)] @1: Anne is cold.[(((triple1) -> rule5))] Anne is round.[(((triple1) -> rule6))] Fiona is cold.[(((triple3) -> rule5))] Fiona is round.[(((triple3) -> rule6))] @2: Anne is kind.[(((((triple1) -> rule5)) -> rule3))] Anne is not big.[(((((triple1) -> rule5) triple1) -> rule7))] Anne is white.[(((triple1 ((triple1) -> rule6)) -> rule1))] Fiona is kind.[(((((triple3) -> rule5)) -> rule3))] Fiona is not big.[(((((triple3) -> rule5) triple3) -> rule7))] Fiona is white.[(((triple3 ((triple3) -> rule6)) -> rule1))] @3: Anne is red.[(((((((triple1) -> rule5)) -> rule3)) -> rule2))] Fiona is red.[(((((((triple3) -> rule5)) -> rule3)) -> rule2))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not big.
("Anne" "is" "big" "-")
((((triple1) -> (rule5 % int2)) triple1) -> (rule7 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not big.
("Fiona" "is" "big" "-")
((((triple3) -> (rule5 % int2)) triple3) -> (rule7 % int1))
Fiona is not big.
("Fiona" "is" "big" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3