Charlie is young. Erin is white. Fiona is cold. Fiona is furry. Fiona is quiet. Fiona is white. Harry is nice. If something is cold then it is quiet. All cold, quiet things are white. Cold, blue things are furry. Furry things are young. Nice things are cold. If Fiona is blue then Fiona is nice. If Fiona is young and Fiona is furry then Fiona is white. All nice things are blue.
Charlie is young.
("Charlie" "is" "young" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All cold, quiet things are white.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Cold, blue things are furry.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If Fiona is blue then Fiona is nice.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "nice" "+"))
If Fiona is young and Fiona is furry then Fiona is white.
((("Fiona" "is" "young" "+") ("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "white" "+"))
All nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Fiona is white.
True
1
proof
[(triple6 OR ((triple3 triple5) -> rule2) OR ((triple3 ((triple3) -> rule1)) -> rule2) OR ((((triple4) -> rule4) triple4) -> rule7))]
("Fiona" "is" "white" "+")
triple6
((triple3 triple5) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple4) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Charlie is not young.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "young" "-")
triple1
Fiona is young.
True
2
proof
[(((triple4) -> rule4))]
("Fiona" "is" "young" "+")
((triple4) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple4) -> rule4))]
("Fiona" "is" "young" "-")
((triple4) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple7) -> rule5)) -> rule1))]
("Harry" "is" "quiet" "+")
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not furry.
False
5
inv-proof
[(((((triple7) -> rule5) ((triple7) -> rule8)) -> rule3))]
("Harry" "is" "furry" "-")
((((triple7) -> (rule5 % int3)) ((triple7) -> (rule8 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is white.
True
6
proof
[(((((triple7) -> rule5) ((((triple7) -> rule5)) -> rule1)) -> rule2))]
("Harry" "is" "white" "+")
((((triple7) -> (rule5 % int3)) ((((triple7) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not white.
False
6
inv-proof
[(((((triple7) -> rule5) ((((triple7) -> rule5)) -> rule1)) -> rule2))]
("Harry" "is" "white" "-")
((((triple7) -> (rule5 % int3)) ((((triple7) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Fiona is not nice.
Unknown
inv-rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("Fiona" "is" "nice" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Fiona is blue.
Unknown
rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("Fiona" "is" "blue" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Charlie is young.[(triple1)] Erin is white.[(triple2)] Fiona is cold.[(triple3)] Fiona is furry.[(triple4)] Fiona is quiet.[(triple5 OR ((triple3) -> rule1))] Fiona is white.[(triple6 OR ((triple3 triple5) -> rule2) OR ((triple3 ((triple3) -> rule1)) -> rule2) OR ((((triple4) -> rule4) triple4) -> rule7))] Harry is nice.[(triple7)] @1: Fiona is young.[(((triple4) -> rule4))] Harry is blue.[(((triple7) -> rule8))] Harry is cold.[(((triple7) -> rule5))] @2: Harry is furry.[(((((triple7) -> rule5) ((triple7) -> rule8)) -> rule3))] Harry is quiet.[(((((triple7) -> rule5)) -> rule1))] @3: Harry is white.[(((((triple7) -> rule5) ((((triple7) -> rule5)) -> rule1)) -> rule2))] Harry is young.[(((((((triple7) -> rule5) ((triple7) -> rule8)) -> rule3)) -> rule4))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple5
((triple3) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple6
((triple3 triple5) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple4) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Fiona is young.
("Fiona" "is" "young" "+")
((triple4) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple7) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple7) -> (rule5 % int3)) ((triple7) -> (rule8 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple7) -> (rule5 % int3)) ((((triple7) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((((((triple7) -> (rule5 % int4)) ((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4