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