Dave is green. Fiona is not young. Harry is smart. If someone is smart then they are red. If someone is red then they are round. If someone is green then they are smart.
Dave is green.
("Dave" "is" "green" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is smart then they are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is green then they are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Dave is not green.
False
1
inv-proof
[(triple1)]
("Dave" "is" "green" "-")
triple1
Dave is smart.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "red" "-")
((triple3) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Dave is red.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Dave" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Harry" "is" "round" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is round.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not round.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "round" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Fiona is not round.
Unknown
inv-rconc
[@3: Fiona is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is red.
Unknown
rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Dave is green.[(triple1)] Fiona is not young.[(triple2)] Harry is smart.[(triple3)] @1: Dave is smart.[(((triple1) -> rule3))] Harry is red.[(((triple3) -> rule1))] @2: Dave is red.[(((((triple1) -> rule3)) -> rule1))] Harry is round.[(((((triple3) -> rule1)) -> rule2))] @3: Dave is round.[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Fiona is not young.
("Fiona" "is" "young" "-")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple3) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3