Anne is smart. Erin is red. Fiona is young. Harry is red. If someone is quiet and smart then they are cold. If someone is red then they are cold. Young people are red. All quiet, kind people are red. If someone is young and smart then they are green. All red, kind people are young. All cold, red people are green. If someone is quiet then they are young.
Anne is smart.
("Anne" "is" "smart" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
If someone is quiet and smart then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All quiet, kind people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is young and smart then they are green.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
All red, kind people are young.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
All cold, red people are green.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Fiona is young.
True
1
proof
[(triple3)]
("Fiona" "is" "young" "+")
triple3
Harry is not red.
False
1
inv-proof
[(triple4)]
("Harry" "is" "red" "-")
triple4
Erin is cold.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple3) -> rule3))]
("Fiona" "is" "red" "-")
((triple3) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("Fiona" "is" "cold" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not cold.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("Fiona" "is" "cold" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is green.
True
6
proof
[(((((((triple3) -> rule3)) -> rule2) ((triple3) -> rule3)) -> rule7))]
("Fiona" "is" "green" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2)) ((triple3) -> (rule3 % int3))) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is not green.
False
6
inv-proof
[(((((((triple3) -> rule3)) -> rule2) ((triple3) -> rule3)) -> rule7))]
("Fiona" "is" "green" "-")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2)) ((triple3) -> (rule3 % int3))) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Anne is not cold.
Unknown
inv-rconc
[@3: Anne is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule6 <- FAIL)]]
("Anne" "is" "cold" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "young" "+")
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "young" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "young" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Anne is smart.[(triple1)] Erin is red.[(triple2)] Fiona is young.[(triple3)] Harry is red.[(triple4)] @1: Erin is cold.[(((triple2) -> rule2))] Fiona is red.[(((triple3) -> rule3))] Harry is cold.[(((triple4) -> rule2))] @2: Erin is green.[(((((triple2) -> rule2) triple2) -> rule7))] Fiona is cold.[(((((triple3) -> rule3)) -> rule2))] Harry is green.[(((((triple4) -> rule2) triple4) -> rule7))] @3: Fiona is green.[(((((((triple3) -> rule3)) -> rule2) ((triple3) -> rule3)) -> rule7))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2)) ((triple3) -> (rule3 % int3))) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3