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