Bob is big. Dave is blue. Fiona is blue. Harry is not blue. All smart people are not furry. If someone is big then they are not furry. If someone is nice then they are big. If someone is blue then they are cold. All blue people are nice. Nice people are blue.
Bob is big.
("Bob" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
All smart people are not furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "-"))
If someone is big then they are not furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "-"))
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is blue then they are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Dave is not blue.
False
1
inv-proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Fiona is nice.
True
2
proof
[(((triple3) -> rule5))]
("Fiona" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Bob is furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Dave is big.
True
3
proof
[(((((triple2) -> rule5)) -> rule3))]
("Dave" "is" "big" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Fiona is not big.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule3))]
("Fiona" "is" "big" "-")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not furry.
True
4
proof
[(((((((triple3) -> rule5)) -> rule3)) -> rule2))]
("Fiona" "is" "furry" "-")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Dave is furry.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule3)) -> rule2))]
("Dave" "is" "furry" "+")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Bob" "is" "blue" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "nice" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is big.
Unknown
rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Bob is big.[(triple1)] Dave is blue.[(triple2)] Fiona is blue.[(triple3)] Harry is not blue.[(triple4)] @1: Bob is not furry.[(((triple1) -> rule2))] Dave is cold.[(((triple2) -> rule4))] Dave is nice.[(((triple2) -> rule5))] Fiona is cold.[(((triple3) -> rule4))] Fiona is nice.[(((triple3) -> rule5))] @2: Dave is big.[(((((triple2) -> rule5)) -> rule3))] Fiona is big.[(((((triple3) -> rule5)) -> rule3))] @3: Dave is not furry.[(((((((triple2) -> rule5)) -> rule3)) -> rule2))] Fiona is not furry.[(((((((triple3) -> rule5)) -> rule3)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Harry is not blue.
("Harry" "is" "blue" "-")
triple4
Bob is not furry.
("Bob" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple3) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Dave is not furry.
("Dave" "is" "furry" "-")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Fiona is not furry.
("Fiona" "is" "furry" "-")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3