Dave is green. Fiona is red. Harry is smart. Green things are smart. All blue things are not green. If Harry is not smart and Harry is not green then Harry is red. If something is smart then it is red. Nice things are red. If something is smart and not blue then it is nice. If something is red then it is not nice. If something is green and not smart then it is not furry.
Dave is green.
("Dave" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
All blue things are not green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
If Harry is not smart and Harry is not green then Harry is red.
((("Harry" "is" "smart" "~") ("Harry" "is" "green" "~")) -> ("Harry" "is" "red" "+"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is smart and not blue then it is nice.
((("something" "is" "smart" "+") ("something" "is" "blue" "~")) -> ("something" "is" "nice" "+"))
If something is red then it is not nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "-"))
If something is green and not smart then it is not furry.
((("something" "is" "green" "+") ("something" "is" "smart" "~")) -> ("something" "is" "furry" "-"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Fiona is not red.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "red" "-")
triple2
Fiona is not nice.
True
2
proof
[(((triple2) -> rule7))]
("Fiona" "is" "nice" "-")
((triple2) -> (rule7 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is nice.
False
2
inv-proof
[(((triple2) -> rule7))]
("Fiona" "is" "nice" "+")
((triple2) -> (rule7 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Dave is red.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Dave" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not red.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Dave" "is" "red" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not nice.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule7))]
("Dave" "is" "nice" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is nice.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule7))]
("Dave" "is" "nice" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Dave is green.[(triple1)] Fiona is red.[(triple2)] Harry is smart.[(triple3)] @1: Dave is smart.[(((triple1) -> rule1))] Fiona is not nice.[(((triple2) -> rule7))] Harry is red.[(((triple3) -> rule4))] @2: Dave is red.[(((((triple1) -> rule1)) -> rule4))] Harry is not nice.[(((((triple3) -> rule4)) -> rule7))] @3: Dave is not nice.[(((((((triple1) -> rule1)) -> rule4)) -> rule7))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is not nice.
("Fiona" "is" "nice" "-")
((triple2) -> (rule7 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple3) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Harry is not nice.
("Harry" "is" "nice" "-")
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3