Bob is cold. Charlie is blue. Fiona is not cold. If someone is green then they are round. All furry, young people are round. If Fiona is young and Fiona is green then Fiona is kind. If someone is furry then they are young. If someone is cold then they are furry. If someone is furry and not cold then they are kind. If someone is round then they are kind. If someone is green and not kind then they are blue.
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
All furry, young people are round.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If Fiona is young and Fiona is green then Fiona is kind.
((("Fiona" "is" "young" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "kind" "+"))
If someone is furry then they are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is cold then they are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and not cold then they are kind.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "kind" "+"))
If someone is round then they are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and not kind then they are blue.
((("someone" "is" "green" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "blue" "+"))
Fiona is not cold.
True
1
proof
[(triple3)]
("Fiona" "is" "cold" "-")
triple3
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Bob is furry.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "furry" "-")
((triple1) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("Bob" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not young.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("Bob" "is" "young" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
True
6
proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule4)) -> rule2))]
("Bob" "is" "round" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not round.
False
6
inv-proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule4)) -> rule2))]
("Bob" "is" "round" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "blue" "-")
Charlie is round.
Unknown
rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "round" "+")
Fiona is not kind.
Unknown
inv-rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "kind" "-")
Charlie is young.
Unknown
rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is cold.[(triple1)] Charlie is blue.[(triple2)] Fiona is not cold.[(triple3)] @1: Bob is furry.[(((triple1) -> rule5))] @2: Bob is young.[(((((triple1) -> rule5)) -> rule4))] @3: Bob is round.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule4)) -> rule2))] @4: Bob is kind.[(((((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule4)) -> rule2)) -> rule7))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((((triple1) -> (rule5 % int4)) ((((triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4