Anne is red. Dave is furry. Fiona is smart. Harry is blue. Smart things are nice. If Harry is smart then Harry is blue. All smart, young things are not red. If Fiona is smart and Fiona is not nice then Fiona is not furry. Nice things are young. All furry things are young.
Anne is red.
("Anne" "is" "red" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If Harry is smart then Harry is blue.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "blue" "+"))
All smart, young things are not red.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "-"))
If Fiona is smart and Fiona is not nice then Fiona is not furry.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "nice" "~")) -> ("Fiona" "is" "furry" "-"))
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Harry is not blue.
False
1
inv-proof
[(triple4)]
("Harry" "is" "blue" "-")
triple4
Fiona is nice.
True
2
proof
[(((triple3) -> rule1))]
("Fiona" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple2) -> rule6))]
("Dave" "is" "young" "-")
((triple2) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is young.
True
3
proof
[(((((triple3) -> rule1)) -> rule5))]
("Fiona" "is" "young" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not young.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5))]
("Fiona" "is" "young" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not red.
True
5
proof
[(((triple3 ((((triple3) -> rule1)) -> rule5)) -> rule3))]
("Fiona" "is" "red" "-")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is red.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule1)) -> rule5)) -> rule3))]
("Fiona" "is" "red" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is young.
Unknown
rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Anne" "is" "young" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "nice" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Harry" "is" "young" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is red.[(triple1)] Dave is furry.[(triple2)] Fiona is smart.[(triple3)] Harry is blue.[(triple4)] @1: Dave is young.[(((triple2) -> rule6))] Fiona is nice.[(((triple3) -> rule1))] @2: Fiona is young.[(((((triple3) -> rule1)) -> rule5))] @3: Fiona is not red.[(((triple3 ((((triple3) -> rule1)) -> rule5)) -> rule3))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not red.
("Fiona" "is" "red" "-")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3