Bob is cold. Dave is young. Harry is quiet. Young people are cold. If Dave is white and Dave is smart then Dave is young. If someone is quiet then they are blue. If Bob is cold and Bob is blue then Bob is young. If Harry is quiet and Harry is smart then Harry is rough. All blue, smart people are quiet. White, young people are smart. If someone is cold then they are quiet.
Bob is cold.
("Bob" "is" "cold" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If Dave is white and Dave is smart then Dave is young.
((("Dave" "is" "white" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "young" "+"))
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If Bob is cold and Bob is blue then Bob is young.
((("Bob" "is" "cold" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "young" "+"))
If Harry is quiet and Harry is smart then Harry is rough.
((("Harry" "is" "quiet" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "rough" "+"))
All blue, smart people are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
White, young people are smart.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Dave is young.
True
1
proof
[(triple2)]
("Dave" "is" "young" "+")
triple2
Bob is not cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
Bob is quiet.
True
2
proof
[(((triple1) -> rule8))]
("Bob" "is" "quiet" "+")
((triple1) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "blue" "-")
((triple3) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is blue.
True
3
proof
[(((((triple1) -> rule8)) -> rule3))]
("Bob" "is" "blue" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule8))]
("Dave" "is" "quiet" "-")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Bob is young.
True
5
proof
[(((triple1 ((((triple1) -> rule8)) -> rule3)) -> rule4))]
("Bob" "is" "young" "+")
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Dave is not blue.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule8)) -> rule3))]
("Dave" "is" "blue" "-")
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "smart" "-")
Harry is rough.
Unknown
rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "smart" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "smart" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Bob is cold.[(triple1)] Dave is young.[(triple2)] Harry is quiet.[(triple3)] @1: Bob is quiet.[(((triple1) -> rule8))] Dave is cold.[(((triple2) -> rule1))] Harry is blue.[(((triple3) -> rule3))] @2: Bob is blue.[(((((triple1) -> rule8)) -> rule3))] Dave is quiet.[(((((triple2) -> rule1)) -> rule8))] @3: Bob is young.[(((triple1 ((((triple1) -> rule8)) -> rule3)) -> rule4))] Dave is blue.[(((((((triple2) -> rule1)) -> rule8)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3