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