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