Fiona is blue. Harry is cold. If someone is white then they are quiet. Quiet people are blue. Nice, blue people are kind. All cold people are blue. Blue, cold people are white. If someone is kind then they are quiet.
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Nice, blue people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Blue, cold people are white.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Fiona is blue.
True
1
proof
[(triple1)]
("Fiona" "is" "blue" "+")
triple1
Fiona is not blue.
False
1
inv-proof
[(triple1)]
("Fiona" "is" "blue" "-")
triple1
Harry is blue.
True
2
proof
[(((triple2) -> rule4))]
("Harry" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple2) -> rule4))]
("Harry" "is" "blue" "-")
((triple2) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule5))]
("Harry" "is" "white" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not white.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule5))]
("Harry" "is" "white" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
True
5
proof
[(((((((triple2) -> rule4) triple2) -> rule5)) -> rule1))]
("Harry" "is" "quiet" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not quiet.
False
5
inv-proof
[(((((((triple2) -> rule4) triple2) -> rule5)) -> rule1))]
("Harry" "is" "quiet" "-")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "kind" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@2: Fiona is quiet.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "white" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Fiona is blue.[(triple1)] Harry is cold.[(triple2)] @1: Harry is blue.[(((triple2) -> rule4))] @2: Harry is white.[(((((triple2) -> rule4) triple2) -> rule5))] @3: Harry is quiet.[(((((((triple2) -> rule4) triple2) -> rule5)) -> rule1))]
Fiona is blue.
("Fiona" "is" "blue" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3