Dave is smart. Fiona is smart. Harry is big. Blue, smart people are nice. If someone is furry and smart then they are cold. If someone is big then they are smart. If someone is cold then they are green. All smart people are cold. If Harry is nice and Harry is furry then Harry is big. If someone is furry and nice then they are smart. If Dave is blue then Dave is smart.
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Blue, smart people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry and smart then they are cold.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold then they are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If Harry is nice and Harry is furry then Harry is big.
((("Harry" "is" "nice" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "big" "+"))
If someone is furry and nice then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Dave is blue then Dave is smart.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "smart" "+"))
Dave is smart.
True
1
proof
[(triple1)]
("Dave" "is" "smart" "+")
triple1
Dave is not smart.
False
1
inv-proof
[(triple1)]
("Dave" "is" "smart" "-")
triple1
Dave is cold.
True
2
proof
[(((triple1) -> rule5))]
("Dave" "is" "cold" "+")
((triple1) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple2) -> rule5))]
("Fiona" "is" "cold" "-")
((triple2) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
True
3
proof
[(((((triple2) -> rule5)) -> rule4))]
("Fiona" "is" "green" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not green.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule4))]
("Fiona" "is" "green" "-")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Harry is green.
True
4
proof
[(((((((triple3) -> rule3)) -> rule5)) -> rule4))]
("Harry" "is" "green" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not green.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule5)) -> rule4))]
("Harry" "is" "green" "-")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "nice" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
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" "+")
@0: Dave is smart.[(triple1)] Fiona is smart.[(triple2)] Harry is big.[(triple3)] @1: Dave is cold.[(((triple1) -> rule5))] Fiona is cold.[(((triple2) -> rule5))] Harry is smart.[(((triple3) -> rule3))] @2: Dave is green.[(((((triple1) -> rule5)) -> rule4))] Fiona is green.[(((((triple2) -> rule5)) -> rule4))] Harry is cold.[(((((triple3) -> rule3)) -> rule5))] @3: Harry is green.[(((((((triple3) -> rule3)) -> rule5)) -> rule4))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3