Bob is rough. Bob is round. Bob is smart. Bob is white. Dave is green. Dave is round. Dave is smart. Dave is young. Erin is round. Erin is smart. Erin is white. Erin is young. Harry is smart. Harry is white. Harry is young. If someone is rough and young then they are blue. Rough people are white. If someone is round then they are young.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is rough and young then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Erin is round.
True
1
proof
[(triple9)]
("Erin" "is" "round" "+")
triple9
Erin is not round.
False
1
inv-proof
[(triple9)]
("Erin" "is" "round" "-")
triple9
Bob is young.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "young" "+")
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "young" "-")
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
True
4
proof
[(((triple1 ((triple2) -> rule3)) -> rule1))]
("Bob" "is" "blue" "+")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not blue.
False
4
inv-proof
[(((triple1 ((triple2) -> rule3)) -> rule1))]
("Bob" "is" "blue" "-")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "blue" "-")
Erin is blue.
Unknown
rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "blue" "+")
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Bob is rough.[(triple1)] Bob is round.[(triple2)] Bob is smart.[(triple3)] Bob is white.[(triple4 OR ((triple1) -> rule2))] Dave is green.[(triple5)] Dave is round.[(triple6)] Dave is smart.[(triple7)] Dave is young.[(triple8 OR ((triple6) -> rule3))] Erin is round.[(triple9)] Erin is smart.[(triple10)] Erin is white.[(triple11)] Erin is young.[(triple12 OR ((triple9) -> rule3))] Harry is smart.[(triple13)] Harry is white.[(triple14)] Harry is young.[(triple15)] @1: Bob is young.[(((triple2) -> rule3))] @2: Bob is blue.[(((triple1 ((triple2) -> rule3)) -> rule1))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
((triple6) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple9) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2