Erin is blue. Fiona is big. Fiona is blue. Fiona is kind. Fiona is red. Harry is big. Harry is round. If something is young and nice then it is blue. Blue things are red. If Erin is red then Erin is young.
Erin is blue.
("Erin" "is" "blue" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is young and nice then it is blue.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If Erin is red then Erin is young.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "young" "+"))
Harry is round.
True
1
proof
[(triple7)]
("Harry" "is" "round" "+")
triple7
Fiona is not big.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "big" "-")
triple2
Erin is red.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "red" "+")
((triple1) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("Erin" "is" "red" "-")
((triple1) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Erin" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Erin" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is red.
Unknown
rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "red" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Erin is blue.[(triple1)] Fiona is big.[(triple2)] Fiona is blue.[(triple3)] Fiona is kind.[(triple4)] Fiona is red.[(triple5 OR ((triple3) -> rule2))] Harry is big.[(triple6)] Harry is round.[(triple7)] @1: Erin is red.[(((triple1) -> rule2))] @2: Erin is young.[(((((triple1) -> rule2)) -> rule3))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4
Fiona is red.
("Fiona" "is" "red" "+")
triple5
((triple3) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
((triple1) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2