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