Bob is big. Dave is kind. Dave is quiet. Erin is nice. Harry is furry. Harry is kind. Harry is nice. All cold people are big. If someone is green then they are big. If Erin is nice then Erin is cold.
Bob is big.
("Bob" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is green then they are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If Erin is nice then Erin is cold.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "cold" "+"))
Erin is nice.
True
1
proof
[(triple4)]
("Erin" "is" "nice" "+")
triple4
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Erin is cold.
True
2
proof
[(((triple4) -> rule3))]
("Erin" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple4) -> rule3))]
("Erin" "is" "cold" "-")
((triple4) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
True
3
proof
[(((((triple4) -> rule3)) -> rule1))]
("Erin" "is" "big" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not big.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule1))]
("Erin" "is" "big" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "big" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is big.[(triple1)] Dave is kind.[(triple2)] Dave is quiet.[(triple3)] Erin is nice.[(triple4)] Harry is furry.[(triple5)] Harry is kind.[(triple6)] Harry is nice.[(triple7)] @1: Erin is cold.[(((triple4) -> rule3))] @2: Erin is big.[(((((triple4) -> rule3)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2