Fiona is quiet. Harry is quiet. Harry is young. If Harry is smart and Harry is white then Harry is quiet. All blue, quiet things are smart. All quiet things are cold. Kind things are cold. If Fiona is smart then Fiona is blue. Young, cold things are white. If something is white then it is blue. If something is white then it is kind.
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is smart and Harry is white then Harry is quiet.
((("Harry" "is" "smart" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "quiet" "+"))
All blue, quiet things are smart.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If Fiona is smart then Fiona is blue.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "blue" "+"))
Young, cold things are white.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is white then it is blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is white then it is kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Harry is young.
True
1
proof
[(triple3)]
("Harry" "is" "young" "+")
triple3
Fiona is not quiet.
False
1
inv-proof
[(triple1)]
("Fiona" "is" "quiet" "-")
triple1
Fiona is cold.
True
2
proof
[(((triple1) -> rule3))]
("Fiona" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple2) -> rule3))]
("Harry" "is" "cold" "-")
((triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
True
4
proof
[(((triple3 ((triple2) -> rule3)) -> rule6))]
("Harry" "is" "white" "+")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not white.
False
4
inv-proof
[(((triple3 ((triple2) -> rule3)) -> rule6))]
("Harry" "is" "white" "-")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Fiona is not kind.
Unknown
inv-rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is smart.
Unknown
rconc
[@3: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule6 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Fiona is quiet.[(triple1)] Harry is quiet.[(triple2)] Harry is young.[(triple3)] @1: Fiona is cold.[(((triple1) -> rule3))] Harry is cold.[(((triple2) -> rule3))] @2: Harry is white.[(((triple3 ((triple2) -> rule3)) -> rule6))] @3: Harry is blue.[(((((triple3 ((triple2) -> rule3)) -> rule6)) -> rule7))] Harry is kind.[(((((triple3 ((triple2) -> rule3)) -> rule6)) -> rule8))] @4: Harry is smart.[(((((((triple3 ((triple2) -> rule3)) -> rule6)) -> rule7) triple2) -> rule2))]
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple3 ((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
((((triple3 ((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple3 ((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule7 % int2)) triple2) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4